let H1, H2 be ZF-formula; :: thesis: variables_in (H1 '&' H2) = (variables_in H1) \/ (variables_in H2)
A1: rng (H1 '&' H2) = (rng (<*3*> ^ H1)) \/ (rng H2) by FINSEQ_1:44
.= ((rng <*3*>) \/ (rng H1)) \/ (rng H2) by FINSEQ_1:44
.= ({3} \/ (rng H1)) \/ (rng H2) by FINSEQ_1:56
.= {3} \/ ((rng H1) \/ (rng H2)) by XBOOLE_1:4 ;
A2: (variables_in H1) \/ (variables_in H2) = ((rng H1) \/ (rng H2)) \ {0 ,1,2,3,4} by XBOOLE_1:42;
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 set ; :: 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 A4: ( a in {3} \/ ((rng H1) \/ (rng H2)) & not a in {0 ,1,2,3,4} & a <> 3 ) by A1, Th150, XBOOLE_0:def 5;
then not a in {3} by TARSKI:def 1;
then a in (rng H1) \/ (rng H2) by A1, A3, XBOOLE_0:def 3;
hence a in (variables_in H1) \/ (variables_in H2) by A2, A4, XBOOLE_0:def 5; :: thesis: verum

end;

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