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