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 A1, A2, RELAT_2:def 9, RELAT_2:def 14;
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 b₁ being Element of the carrier of P st
( X is_<=_than b₁ & ( for b₂ being Element of the carrier of P holds
( not X is_<=_than b₂ or b₁ <= b₂ ) ) )
defpred S₁[ 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 & S₁[x] ) ) from XBOOLE_0:sch 1();
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 A2, RELAT_1:15;
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 A1, A2, A6, WELLORD1:6;
reconsider a = a as Element of P by A6, A8;
take a ; :: thesis: ( X is_<=_than a & ( for b₁ being Element of the carrier of P holds
( not X is_<=_than b₁ or a <= b₁ ) ) )
thus for y being Element of P st y in X holds
y <= a by A5, A8; :: according to LATTICE3:def 9 :: thesis: for b₁ being Element of the carrier of P holds
( not X is_<=_than b₁ or a <= b₁ )
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 ORDERS_2:def 5, A10;
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