let H be ZF-formula; :: thesis: variables_in ('not' H) = variables_in H
A1: rng ('not' H) = (rng <*2*>) \/ (rng H) by FINSEQ_1:31
.= {2} \/ (rng H) by FINSEQ_1:39 ;
thus variables_in ('not' H) c= variables_in H :: according to XBOOLE_0:def 10 :: thesis: variables_in H c= variables_in ('not' H)
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in variables_in ('not' H) or a in variables_in H )
assume A2: a in variables_in ('not' H) ; :: thesis: a in variables_in H
then a <> 2 by Th137;
then not a in {2} by TARSKI:def 1;
then A3: a in rng H by A1, A2, XBOOLE_0:def 3;
not a in {0,1,2,3,4} by A2, XBOOLE_0:def 5;
hence a in variables_in H by A3, XBOOLE_0:def 5; :: thesis: verum
end;
thus variables_in H c= variables_in ('not' H) by A1, XBOOLE_1:7, XBOOLE_1:33; :: thesis: verum