defpred S₁[ set , set ] means ex T being quasi-type of C st
( $1 = T & $2 = vars T );
A3: for x being set st x in QuasiTypes C holds
ex y being set st S₁[x,y]

proof

let x be set ; :: thesis: ( x in QuasiTypes C implies ex y being set st S₁[x,y] )
assume x in QuasiTypes C ; :: thesis: ex y being set st S₁[x,y]
then reconsider T = x as quasi-type of C by Def43;
take y = vars T; :: thesis: S₁[x,y]
take T ; :: thesis: ( x = T & y = vars T )
thus ( x = T & y = vars T ) ; :: thesis: verum

end;

consider f being Function such that
A4: dom f = QuasiTypes C and
A5: for x being set st x in QuasiTypes C holds
S₁[x,f . x] from CLASSES1:sch 1(A3);
rng f c= the carrier of VarPoset

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in the carrier of VarPoset )
assume y in rng f ; :: thesis: y in the carrier of VarPoset
then consider x being set such that
A6: x in dom f and
A7: y = f . x by FUNCT_1:def 5;
consider T being quasi-type of C such that
x = T and
A8: y = vars T by A4, A5, A6, A7;
varcl (vars T) = vars T ;
then y is Element of VarPoset by A8, Th110;
hence y in the carrier of VarPoset ; :: thesis: verum

end;

then reconsider f = f as Function of (QuasiTypes C),the carrier of VarPoset by A4, FUNCT_2:4;
take f ; :: thesis: for T being quasi-type of C holds f . T = vars T
let x be quasi-type of C; :: thesis: f . x = vars x
x in QuasiTypes C by Def43;
then ex T being quasi-type of C st
( x = T & f . x = vars T ) by A5;
hence f . x = vars x ; :: thesis: verum