let H be ZF-formula; :: thesis: for x being Variable holds variables_in (All x,H) = (variables_in H) \/ {x}
let x be Variable; :: thesis: variables_in (All x,H) = (variables_in H) \/ {x}
A1: rng (All x,H) = (rng (<*4*> ^ <*x*>)) \/ (rng H) by FINSEQ_1:44
.= ((rng <*4*>) \/ (rng <*x*>)) \/ (rng H) by FINSEQ_1:44
.= ({4} \/ (rng <*x*>)) \/ (rng H) by FINSEQ_1:56
.= ({4} \/ {x}) \/ (rng H) by FINSEQ_1:56
.= {4} \/ ({x} \/ (rng H)) by XBOOLE_1:4 ;
thus variables_in (All x,H) c= (variables_in H) \/ {x} :: according to XBOOLE_0:def 10 :: thesis: (variables_in H) \/ {x} c= variables_in (All x,H)

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in variables_in (All x,H) or a in (variables_in H) \/ {x} )
assume A2: a in variables_in (All x,H) ; :: thesis: a in (variables_in H) \/ {x}
then A3: ( a in {4} \/ ({x} \/ (rng H)) & not a in {0 ,1,2,3,4} & a <> 4 ) by A1, Th150, XBOOLE_0:def 5;
then not a in {4} by TARSKI:def 1;
then a in {x} \/ (rng H) by A1, A2, XBOOLE_0:def 3;
then ( ( a in {x} or a in rng H ) & ( a in rng H implies a in variables_in H ) ) by A3, XBOOLE_0:def 3, XBOOLE_0:def 5;
hence a in (variables_in H) \/ {x} by XBOOLE_0:def 3; :: thesis: verum

end;

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in (variables_in H) \/ {x} or a in variables_in (All x,H) )
assume a in (variables_in H) \/ {x} ; :: thesis: a in variables_in (All x,H)
then ( a in variables_in H or a in {x} ) by XBOOLE_0:def 3;
then ( ( a in rng H & not a in {0 ,1,2,3,4} ) or ( a in {x} & x = a ) ) by TARSKI:def 1, XBOOLE_0:def 5;
then A4: ( a in {x} \/ (rng H) & not a in {0 ,1,2,3,4} ) by Th149, XBOOLE_0:def 3;
then a in {4} \/ ({x} \/ (rng H)) by XBOOLE_0:def 3;
hence a in variables_in (All x,H) by A1, A4, XBOOLE_0:def 5; :: thesis: verum