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:31
.= ((rng <*1*>) \/ (rng <*x*>)) \/ (rng <*y*>) by FINSEQ_1:31
.= ({1} \/ (rng <*x*>)) \/ (rng <*y*>) by FINSEQ_1:39
.= ({1} \/ {x}) \/ (rng <*y*>) by FINSEQ_1:39
.= ({1} \/ {x}) \/ {y} by FINSEQ_1:39
.= {1} \/ ({x} \/ {y}) by XBOOLE_1:4
.= {1} \/ {x,y} by ENUMSET1:1 ;
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 object ; :: 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 <> 1 by Th137;
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 object ; :: according to TARSKI:def 3 :: thesis: ( not a in {x,y} or a in variables_in (x 'in' y) )
assume A3: a in {x,y} ; :: thesis: a in variables_in (x 'in' 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 {1} \/ {x,y} by A3, XBOOLE_0:def 3;
hence a in variables_in (x 'in' y) by A1, A4, XBOOLE_0:def 5; :: thesis: verum