let x, y be Variable; :: thesis: variables_in (x '=' y) = {x,y}
A1: rng (x '=' y) = (rng (<*0 *> ^ <*x*>)) \/ (rng <*y*>) by FINSEQ_1:44
.= ((rng <*0 *>) \/ (rng <*x*>)) \/ (rng <*y*>) by FINSEQ_1:44
.= ({0 } \/ (rng <*x*>)) \/ (rng <*y*>) by FINSEQ_1:56
.= ({0 } \/ {x}) \/ (rng <*y*>) by FINSEQ_1:56
.= ({0 } \/ {x}) \/ {y} by FINSEQ_1:56
.= {0 } \/ ({x} \/ {y}) by XBOOLE_1:4
.= {0 } \/ {x,y} by ENUMSET1:41 ;
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 set ; :: 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 in {0 } \/ {x,y} & a <> 0 ) by A1, Th150;
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 set ; :: according to TARSKI:def 3 :: thesis: ( not a in {x,y} or a in variables_in (x '=' y) )
assume a in {x,y} ; :: thesis: a in variables_in (x '=' y)
then A3: ( a in {0 } \/ {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 '=' y) by A1, A3, XBOOLE_0:def 5; :: thesis: verum