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:100;
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 )
( the InternalRel of P is connected & the InternalRel of P is reflexive ) by A1;
then ( the InternalRel of P is_connected_in the carrier of P & the InternalRel of P is_reflexive_in the carrier of P & ( x = y or x <> y ) ) by 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 RELAT_2:def 1, RELAT_2:def 6;
hence ( x <= y or y <= x ) by ORDERS_2:def 9; :: thesis: verum

end;

thus P is complete :: thesis: P is continuous

proof

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₁[ set ] 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
A4: for x being set holds
( x in Y iff ( x in the carrier of P & S₁[x] ) ) from XBOOLE_0:sch 1();
the InternalRel of P is upper-bounded by Th8;
then consider x being set such that
A5: for y being set st y in field the InternalRel of P holds
[y,x] in the InternalRel of P by Def9;
consider y being Element of P;
[y,x] in the InternalRel of P by A2, A5;
then reconsider x = x as Element of P by A2, RELAT_1:30;
A6: Y c= the carrier of P

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Y or x in the carrier of P )
thus ( not x in Y or x in the carrier of P ) by A4; :: thesis: verum

end;

for y being Element of P st y in X holds
[y,x] in the InternalRel of P by A2, A5;
then x in Y by A4;
then consider a being set such that
A7: ( a in Y & ( for b being set st b in Y holds
[a,b] in the InternalRel of P ) ) by A1, A2, A6, WELLORD1:10;
reconsider a = a as Element of P by A6, A7;
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₁ ) ) )

hereby :: 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 y be Element of P; :: thesis: ( y in X implies y <= a )
assume y in X ; :: thesis: y <= a
then [y,a] in the InternalRel of P by A4, A7;
hence y <= a by ORDERS_2:def 9; :: thesis: verum

end;

let b be Element of P; :: thesis: ( not X is_<=_than b or a <= b )
assume A8: for c being Element of P st c in X holds
c <= b ; :: according to LATTICE3:def 9 :: thesis: a <= b

now

let c be Element of P; :: thesis: ( c in X implies [c,b] in the InternalRel of P )
assume c in X ; :: thesis: [c,b] in the InternalRel of P
then c <= b by A8;
hence [c,b] in the InternalRel of P by ORDERS_2:def 9; :: thesis: verum

end;

then b in Y by A4;
then [a,b] in the InternalRel of P by A7;
hence a <= b by ORDERS_2:def 9; :: thesis: verum

end;

then P is complete Chain by A3;
hence P is continuous ; :: thesis: verum