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

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in variables_in (x '=' y) or a in {x,y} )
assume A2: a in variables_in (x '=' y) ; :: thesis: a in {x,y}
then a <> 0 by Th137;
then not a in {0} by TARSKI:def 1;
hence a in {x,y} by A1, A2, XBOOLE_0:def 3; :: thesis: verum

end;

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