defpred S_{2}[ object , object ] means ex P being strict Poset st

( $2 = P & the InternalRel of P = $1 );

defpred S_{3}[ set , set ] means $2 is Order of $1;

deffunc H_{1}( 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_{1}(x) & S_{3}[x,y] ) )
from CARD_3:sch 3();

A8: for x being object holds

( x in A iff ex y being object st

( y in Union F & S_{2}[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 ) )

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

( $2 = P & the InternalRel of P = $1 );

defpred S

deffunc H

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

A5: now :: thesis: for x, y, z being object st S_{2}[x,y] & S_{2}[x,z] holds

y = z

consider A being set such that y = z

let x, y, z be object ; :: thesis: ( S_{2}[x,y] & S_{2}[x,z] implies y = z )

assume S_{2}[x,y]
; :: thesis: ( S_{2}[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_{2}[x,z]
; :: thesis: y = z

hence y = z by A6, A7, ORDERS_1:14; :: thesis: verum

end;assume S

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

hence y = z by A6, A7, ORDERS_1:14; :: thesis: verum

A8: for x being object holds

( x in A iff ex y being object st

( y in Union F & S

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 that 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;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

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