let x, y be Variable; :: thesis: variables_in (x 'in' y) = {x,y}
A1: rng (x 'in' y) = (rng (<*1*> ^ <*x*>)) \/ (rng <*y*>) by FINSEQ_1:44
.= ((rng <*1*>) \/ (rng <*x*>)) \/ (rng <*y*>) by FINSEQ_1:44
.= ({1} \/ (rng <*x*>)) \/ (rng <*y*>) by FINSEQ_1:56
.= ({1} \/ {x}) \/ (rng <*y*>) by FINSEQ_1:56
.= ({1} \/ {x}) \/ {y} by FINSEQ_1:56
.= {1} \/ ({x} \/ {y}) by XBOOLE_1:4
.= {1} \/ {x,y} by ENUMSET1:41 ;
thus variables_in (x 'in' y) c= {x,y} :: according to XBOOLE_0:def 10 :: thesis: {x,y} c= variables_in (x 'in' y)

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in variables_in (x 'in' y) or a in {x,y} )
assume A2: a in variables_in (x 'in' y) ; :: thesis: a in {x,y}
then ( a in {1} \/ {x,y} & a <> 1 ) by A1, Th150;
then not a in {1} by TARSKI:def 1;
hence a in {x,y} by A1, A2, XBOOLE_0:def 3; :: thesis: verum

end;

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