let H be ZF-formula; :: thesis: for E being non empty set st H is negative holds
for f being Function of VAR,E holds
( not f in St ((the_argument_of H),E) iff f in St (H,E) )
let E be non empty set ; :: thesis: ( H is negative implies for f being Function of VAR,E holds
( not f in St ((the_argument_of H),E) iff f in St (H,E) ) )
assume H is negative ; :: thesis: for f being Function of VAR,E holds
( not f in St ((the_argument_of H),E) iff f in St (H,E) )
then H = 'not' (the_argument_of H) by ZF_LANG:def 30;
hence for f being Function of VAR,E holds
( not f in St ((the_argument_of H),E) iff f in St (H,E) ) by Th4; :: thesis: verum