let H1, H2 be ZF-formula; :: thesis: variables_in (H1 '&' H2) = (variables_in H1) \/ (variables_in H2)
A1: (variables_in H1) \/ (variables_in H2) = ((rng H1) \/ (rng H2)) \ {0,1,2,3,4} by XBOOLE_1:42;
A2: rng (H1 '&' H2) = (rng (<*3*> ^ H1)) \/ (rng H2) by FINSEQ_1:31
.= ((rng <*3*>) \/ (rng H1)) \/ (rng H2) by FINSEQ_1:31
.= ({3} \/ (rng H1)) \/ (rng H2) by FINSEQ_1:39
.= {3} \/ ((rng H1) \/ (rng H2)) by XBOOLE_1:4 ;
thus variables_in (H1 '&' H2) c= (variables_in H1) \/ (variables_in H2) :: according to XBOOLE_0:def 10 :: thesis: (variables_in H1) \/ (variables_in H2) c= variables_in (H1 '&' H2)

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in variables_in (H1 '&' H2) or a in (variables_in H1) \/ (variables_in H2) )
assume A3: a in variables_in (H1 '&' H2) ; :: thesis: a in (variables_in H1) \/ (variables_in H2)
then a <> 3 by Th137;
then not a in {3} by TARSKI:def 1;
then A4: a in (rng H1) \/ (rng H2) by A2, A3, XBOOLE_0:def 3;
not a in {0,1,2,3,4} by A3, XBOOLE_0:def 5;
hence a in (variables_in H1) \/ (variables_in H2) by A1, A4, XBOOLE_0:def 5; :: thesis: verum

end;

thus (variables_in H1) \/ (variables_in H2) c= variables_in (H1 '&' H2) by A2, A1, XBOOLE_1:7, XBOOLE_1:33; :: thesis: verum