defpred S₂[ object , object ] means ex P being strict Poset st
( $2 = P & the InternalRel of P = $1 );
defpred S₃[ set , set ] means $2 is Order of $1;
deffunc H₁( 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 H₁(x) & S₃[x,y] ) ) from CARD_3:sch 3();

A5: now :: thesis: for x, y, z being object st S₂[x,y] & S₂[x,z] holds
y = z

let x, y, z be object ; :: thesis: ( S₂[x,y] & S₂[x,z] implies y = z )
assume S₂[x,y] ; :: thesis: ( S₂[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 S₂[x,z] ; :: thesis: y = z
hence y = z by A6, A7, ORDERS_1:14; :: 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 & S₂[y,x] ) ) from TARSKI:sch 1(A5);
take A ; :: thesis: for x being object holds
( x in A iff ( x is strict Poset & the carrier of (x as_1-sorted) in W ) )
let x be object ; :: thesis: ( x in A iff ( x is strict Poset & the carrier of (x as_1-sorted) in W ) )

hereby :: thesis: ( x is strict Poset & the carrier of (x as_1-sorted) in W implies x in A )

assume x in A ; :: thesis: ( x is strict Poset & the carrier of (x as_1-sorted) 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 (x as_1-sorted) in W
consider z being object such that
A13: z in W and
A14: y in F . z by A3, A9, CARD_5:2;
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 A12, ORDERS_1:14;
hence the carrier of (x as_1-sorted) in W by A11, A13, Def1; :: thesis: verum

end;

assume that
A15: x is strict Poset and
A16: the carrier of (x as_1-sorted) 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 A4, A16;
then the InternalRel of P in Union F by A3, A16, A17, CARD_5:2;
hence x in A by A8; :: thesis: verum