defpred S2[ object , object ] means ex P being strict Poset st
( \$2 = P & the InternalRel of P = \$1 );
defpred S3[ set , set ] means \$2 is Order of \$1;
deffunc H1( set ) -> set = bool [:\$1,\$1:];
consider F being Function such that
A3: dom F = W and
A4: for x being set st x in W holds
for y being set holds
( y in F . x iff ( y in H1(x) & S3[x,y] ) ) from CARD_3:sch 3();
A5: now :: thesis: for x, y, z being object st S2[x,y] & S2[x,z] holds
y = z
let x, y, z be object ; :: thesis: ( S2[x,y] & S2[x,z] implies y = z )
assume S2[x,y] ; :: thesis: ( S2[x,z] implies y = z )
then consider P1 being strict Poset such that
A6: ( y = P1 & the InternalRel of P1 = x ) ;
A7: dom the InternalRel of P1 = the carrier of P1 by ORDERS_1:14;
assume S2[x,z] ; :: thesis: y = z
hence y = z by ; :: thesis: verum
end;
consider A being set such that
A8: for x being object holds
( x in A iff ex y being object st
( y in Union F & S2[y,x] ) ) from take A ; :: thesis: for x being object holds
( x in A iff ( x is strict Poset & the carrier of () in W ) )

let x be object ; :: thesis: ( x in A iff ( x is strict Poset & the carrier of () in W ) )
hereby :: thesis: ( x is strict Poset & the carrier of () in W implies x in A )
assume x in A ; :: thesis: ( x is strict Poset & the carrier of () in W )
then consider y being object such that
A9: y in Union F and
A10: ex P being strict Poset st
( x = P & the InternalRel of P = y ) by A8;
consider P being strict Poset such that
A11: x = P and
A12: the InternalRel of P = y by A10;
thus x is strict Poset by A11; :: thesis: the carrier of () in W
consider z being object such that
A13: z in W and
A14: y in F . z by ;
reconsider z = z as set by TARSKI:1;
reconsider y = y as Order of z by A4, A13, A14;
( dom y = z & dom y = the carrier of P ) by ;
hence the carrier of () in W by ; :: thesis: verum
end;
assume that
A15: x is strict Poset and
A16: the carrier of () in W ; :: thesis: x in A
reconsider P = x as strict Poset by A15;
A17: x as_1-sorted = P by Def1;
then the InternalRel of P in F . the carrier of P by ;
then the InternalRel of P in Union F by ;
hence x in A by A8; :: thesis: verum