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 )

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

thus
P is complete
:: thesis: P is continuous
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;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

proof

hence
P is continuous
by A3; :: thesis: verum
set y = the Element of P;

let X be set ; :: according to LATTICE3:def 12 :: thesis: ex b_{1} being Element of the carrier of P st

( X is_<=_than b_{1} & ( for b_{2} being Element of the carrier of P holds

( not X is_<=_than b_{2} or b_{1} <= b_{2} ) ) )

defpred S_{1}[ 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_{1}[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_{1} being Element of the carrier of P holds

( not X is_<=_than b_{1} or a <= b_{1} ) ) )

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_{1} being Element of the carrier of P holds

( not X is_<=_than b_{1} or a <= b_{1} )

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;let X be set ; :: according to LATTICE3:def 12 :: thesis: ex b

( X is_<=_than b

( not X is_<=_than b

defpred S

[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

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

( not X is_<=_than 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

( not X is_<=_than 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