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:31
.= ((rng <*4*>) \/ (rng <*x*>)) \/ (rng H) by FINSEQ_1:31
.= ({4} \/ (rng <*x*>)) \/ (rng H) by FINSEQ_1:39
.= ({4} \/ {x}) \/ (rng H) by FINSEQ_1:39
.= {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 object ; :: 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 a <> 4 by Th137;
then not a in {4} by TARSKI:def 1;
then a in {x} \/ (rng H) by A1, A2, XBOOLE_0:def 3;
then A3: ( a in {x} or a in rng H ) by XBOOLE_0:def 3;
not a in {0,1,2,3,4} by A2, XBOOLE_0:def 5;
then ( a in rng H implies a in variables_in H ) by XBOOLE_0:def 5;
hence a in (variables_in H) \/ {x} by A3, XBOOLE_0:def 3; :: thesis: verum

end;

let a be object ; :: 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 A4: ( a in variables_in H or a in {x} ) by XBOOLE_0:def 3;
then a in {x} \/ (rng H) by XBOOLE_0:def 3;
then A5: a in {4} \/ ({x} \/ (rng H)) by XBOOLE_0:def 3;
( ( a in rng H & not a in {0,1,2,3,4} ) or ( a in {x} & x = a ) ) by A4, TARSKI:def 1, XBOOLE_0:def 5;
then not a in {0,1,2,3,4} by Th136;
hence a in variables_in (All (x,H)) by A1, A5, XBOOLE_0:def 5; :: thesis: verum