let P be non empty upper-bounded Poset; :: thesis: ( the InternalRel of P is well-ordering implies ( P is connected & P is complete & P is continuous ) )
assume A1: the InternalRel of P is well-ordering ; :: thesis: ( P is connected & P is complete & P is continuous )
A2: field the InternalRel of P = the carrier of P by ORDERS_1:15;
thus A3: P is connected :: thesis: ( P is complete & P is continuous )
proof
let x, y be Element of P; :: according to WAYBEL_0:def 29 :: thesis: ( x <= y or y <= x )
A4: ( x = y or x <> y ) ;
( the InternalRel of P is_connected_in the carrier of P & the InternalRel of P is_reflexive_in the carrier of P ) by ;
then ( [x,y] in the InternalRel of P or [y,x] in the InternalRel of P ) by A4;
hence ( x <= y or y <= x ) ; :: thesis: verum
end;
thus P is complete :: thesis: P is continuous
proof
set y = the Element of P;
let X be set ; :: according to LATTICE3:def 12 :: thesis: ex b1 being Element of the carrier of P st
( X is_<=_than b1 & ( for b2 being Element of the carrier of P holds
( not X is_<=_than b2 or b1 <= b2 ) ) )

defpred S1[ object ] means for y being Element of P st y in X holds
[y,\$1] in the InternalRel of P;
consider Y being set such that
A5: for x being object holds
( x in Y iff ( x in the carrier of P & S1[x] ) ) from A6: Y c= the carrier of P by A5;
the InternalRel of P is upper-bounded by Th8;
then consider x being set such that
A7: for y being set st y in field the InternalRel of P holds
[y,x] in the InternalRel of P ;
[ the Element of P,x] in the InternalRel of P by A2, A7;
then reconsider x = x as Element of P by ;
for y being Element of P st y in X holds
[y,x] in the InternalRel of P by A2, A7;
then x in Y by A5;
then consider a being object such that
A8: a in Y and
A9: for b being object st b in Y holds
[a,b] in the InternalRel of P by ;
reconsider a = a as Element of P by A6, A8;
take a ; :: thesis: ( X is_<=_than a & ( for b1 being Element of the carrier of P holds
( not X is_<=_than b1 or a <= b1 ) ) )

thus for y being Element of P st y in X holds
y <= a by A5, A8; :: according to LATTICE3:def 9 :: thesis: for b1 being Element of the carrier of P holds
( not X is_<=_than b1 or a <= b1 )

let b be Element of P; :: thesis: ( not X is_<=_than b or a <= b )
assume A10: for c being Element of P st c in X holds
c <= b ; :: according to LATTICE3:def 9 :: thesis: a <= b
for c being Element of P st c in X holds
[c,b] in the InternalRel of P by ;
then b in Y by A5;
then [a,b] in the InternalRel of P by A9;
hence a <= b ; :: thesis: verum
end;
hence P is continuous by A3; :: thesis: verum