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 for x, y, z being object st S2[x,y] & S2[x,z] holds
y = zend;
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 TARSKI:sch 1(A5);
take
A
; 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 ; ( x in A iff ( x is strict Poset & the carrier of (x as_1-sorted) in W ) )
assume that
A15:
x is strict Poset
and
A16:
the carrier of (x as_1-sorted) in W
; 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; verum