let l be quasi-loci; :: thesis: varcl (rng l) = rng l

now

let x, y be set ; :: thesis: ( [x,y] in rng l implies x c= rng l )
assume A2: [x,y] in rng l ; :: thesis: x c= rng l
then reconsider xy = [x,y] as variable ;
consider i being set such that
A3: ( i in dom l & xy = l . i ) by A2, FUNCT_1:def 5;
reconsider i = i as Nat by A3;
A5: vars xy = x by MCART_1:7;
thus x c= rng l :: thesis: verum

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in x or a in rng l )
assume A6: a in x ; :: thesis: a in rng l
then reconsider a = a as variable by A5;
ex j being Nat st
( j in dom l & j < i & a = l . j ) by A3, A5, A6, Th32;
hence a in rng l by FUNCT_1:def 5; :: thesis: verum

end;

end;

hence varcl (rng l) c= rng l by VARCL; :: according to XBOOLE_0:def 10 :: thesis: rng l c= varcl (rng l)
thus rng l c= varcl (rng l) by VARCL; :: thesis: verum