let X be finite Subset of Vars; :: thesis: ex l being quasi-loci st rng l = varcl X
reconsider Y = varcl X as finite Subset of Vars by ABCMIZ_1:24;
defpred S1[ set , set ] means $1 in $2 `1 ;
A1: for x, y being set st x in Y & y in Y & S1[x,y] holds
not S1[y,x]
proof
let x, y be set ; :: thesis: ( x in Y & y in Y & S1[x,y] implies not S1[y,x] )
assume A2: ( x in Y & y in Y & S1[x,y] & S1[y,x] ) ; :: thesis: contradiction
x in Vars by A2;
then consider A being Subset of Vars, j being Element of NAT such that
A3: ( x = [(varcl A),j] & A is finite ) by ABCMIZ_1:18;
y in Vars by A2;
then consider B being Subset of Vars, k being Element of NAT such that
A4: ( y = [(varcl B),k] & B is finite ) by ABCMIZ_1:18;
A5: ( y in varcl A & x in varcl B ) by A2, A3, A4;
A6: ( varcl A in {(varcl A)} & varcl B in {(varcl B)} ) by TARSKI:def 1;
( {(varcl A)} in x & {(varcl B)} in y ) by A4, A3, TARSKI:def 2;
hence contradiction by A5, A6, XREGULAR:10; :: thesis: verum
end;
A7: for x, y, z being set st x in Y & y in Y & z in Y & S1[x,y] & S1[y,z] holds
S1[x,z]
proof
let x, y, z be set ; :: thesis: ( x in Y & y in Y & z in Y & S1[x,y] & S1[y,z] implies S1[x,z] )
assume A8: ( x in Y & y in Y & z in Y & S1[x,y] & S1[y,z] ) ; :: thesis: S1[x,z]
y in Vars by A8;
then consider B being Subset of Vars, k being Element of NAT such that
A9: ( y = [(varcl B),k] & B is finite ) by ABCMIZ_1:18;
z in Vars by A8;
then consider C being Subset of Vars, j being Element of NAT such that
A10: ( z = [(varcl C),j] & C is finite ) by ABCMIZ_1:18;
A11: ( z `1 = varcl C & y `1 = varcl B ) by A10, A9;
then varcl B c= varcl C by A8, A9, ABCMIZ_1:def 1;
hence S1[x,z] by A11, A8; :: thesis: verum
end;
consider l being one-to-one FinSequence such that
A12: rng l = Y and
A13: for i, j being Nat st i in dom l & j in dom l & S1[l . i,l . j] holds
i < j from ABCMIZ_A:sch 3(A1, A7);
 reconsider l = l as one-to-one FinSequence of Vars by A12, FINSEQ_1:def 4;
now :: thesis: for i being Nat
for x being variable st i in dom l & x = l . i holds
for y being variable st y in vars x holds
ex a being Nat st
( a in dom l & a < i & y = l . a )
let i be Nat; :: thesis: for x being variable st i in dom l & x = l . i holds
for y being variable st y in vars x holds
ex a being Nat st
( a in dom l & a < i & y = l . a )
let x be variable; :: thesis: ( i in dom l & x = l . i implies for y being variable st y in vars x holds
ex a being Nat st
( a in dom l & a < i & y = l . a ) )
assume A14: ( i in dom l & x = l . i ) ; :: thesis: for y being variable st y in vars x holds
ex a being Nat st
( a in dom l & a < i & y = l . a )
let y be variable; :: thesis: ( y in vars x implies ex a being Nat st
( a in dom l & a < i & y = l . a ) )
assume A15: y in vars x ; :: thesis: ex a being Nat st
( a in dom l & a < i & y = l . a )
x in Vars ;
then consider A being Subset of Vars, j being Element of NAT such that
A16: ( x = [(varcl A),j] & A is finite ) by ABCMIZ_1:18;
( x in rng l & vars x = varcl A ) by A14, A16, FUNCT_1:def 3;
then vars x c= Y by A12, A16, ABCMIZ_1:def 1;
then consider a being object such that
A17: ( a in dom l & y = l . a ) by A12, A15, FUNCT_1:def 3;
reconsider a = a as Nat by A17;
take a = a; :: thesis: ( a in dom l & a < i & y = l . a )
thus ( a in dom l & a < i & y = l . a ) by A13, A14, A15, A17; :: thesis: verum
end;
then reconsider l = l as quasi-loci by ABCMIZ_1:30;
take l ; :: thesis: rng l = varcl X
thus rng l = varcl X by A12; :: thesis: verum