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 A1: [x,y] in rng l ; :: thesis: x c= rng l
then reconsider xy = [x,y] as variable ;
consider i being set such that
A2: i in dom l and
A3: xy = l . i by A1, FUNCT_1:def 3;
reconsider i = i as Nat by A2;
A4: 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 A5: a in x ; :: thesis: a in rng l
then reconsider a = a as variable by A4;
ex j being Nat st
( j in dom l & j < i & a = l . j ) by A2, A3, A4, A5, Th30;
hence a in rng l by FUNCT_1:def 3; :: thesis: verum

end;

end;

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