import proveit
from proveit import defaults
from proveit import x, A, S
from proveit.logic import InSet
from proveit.logic.booleans.negation import closure
from proveit.logic.sets.membership import not_in_set_def
theory = proveit.Theory() # the theorem's theory
%proving not_in_set_is_bool
defaults.assumptions = not_in_set_is_bool.all_conditions()
closure
closure_spec = closure.instantiate({A:InSet(x, S)})
not_in_set_def
not_in_set_def_spec = not_in_set_def.instantiate({x:x, S:S})
not_in_set_def_spec.sub_left_side_into(closure_spec)
%qed