let x, y be Variable; 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}
XBOOLE_0:def 10 {x,y} c= variables_in (x 'in' y)
let a be object ; TARSKI:def 3 ( not a in {x,y} or a in variables_in (x 'in' y) )
assume A3:
a in {x,y}
; 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; verum