let P be non empty upper-bounded Poset; :: thesis: ( the InternalRel of P is well-ordering implies for x, y being Element of P st y < x holds

ex z being Element of P st

( z is compact & y <= z & z <= x ) )

set R = the InternalRel of P;

set A = order_type_of the InternalRel of P;

A1: field (RelIncl (order_type_of the InternalRel of P)) = order_type_of the InternalRel of P by WELLORD2:def 1;

assume A2: the InternalRel of P is well-ordering ; :: thesis: for x, y being Element of P st y < x holds

ex z being Element of P st

( z is compact & y <= z & z <= x )

then reconsider L = P as complete Chain by Th9;

let x, y be Element of P; :: thesis: ( y < x implies ex z being Element of P st

( z is compact & y <= z & z <= x ) )

the InternalRel of P, RelIncl (order_type_of the InternalRel of P) are_isomorphic by A2, WELLORD2:def 2;

then consider f being Function such that

A3: f is_isomorphism_of the InternalRel of P, RelIncl (order_type_of the InternalRel of P) ;

assume A4: y < x ; :: thesis: ex z being Element of P st

( z is compact & y <= z & z <= x )

then y <= x ;

then A5: [y,x] in the InternalRel of P ;

then A6: [(f . y),(f . x)] in RelIncl (order_type_of the InternalRel of P) by A3;

then A7: f . x in order_type_of the InternalRel of P by A1, RELAT_1:15;

A8: f . x <> f . y by A3, A4, A5, WELLORD1:36;

A9: f . y in order_type_of the InternalRel of P by A6, A1, RELAT_1:15;

then reconsider a = f . x, b = f . y as Ordinal by A7;

b c= a by A6, A7, A9, WELLORD2:def 1;

then b c< a by A8;

then b in a by ORDINAL1:11;

then A10: succ b c= a by ORDINAL1:21;

then A11: succ b in order_type_of the InternalRel of P by A7, ORDINAL1:12;

then A12: [(succ b),(f . x)] in RelIncl (order_type_of the InternalRel of P) by A7, A10, WELLORD2:def 1;

A13: b c= succ b by ORDINAL3:1;

rng f = order_type_of the InternalRel of P by A3, A1;

then consider z being object such that

A14: z in dom f and

A15: succ b = f . z by A11, FUNCT_1:def 3;

A16: field the InternalRel of P = the carrier of P by ORDERS_1:15;

then reconsider z = z as Element of P by A3, A14;

take z ; :: thesis: ( z is compact & y <= z & z <= x )

A17: dom f = field the InternalRel of P by A3;

thus z is compact :: thesis: ( y <= z & z <= x )

hence ( [y,z] in the InternalRel of P & [z,x] in the InternalRel of P ) by A3, A15, A16, A12; :: according to ORDERS_2:def 5 :: thesis: verum

ex z being Element of P st

( z is compact & y <= z & z <= x ) )

set R = the InternalRel of P;

set A = order_type_of the InternalRel of P;

A1: field (RelIncl (order_type_of the InternalRel of P)) = order_type_of the InternalRel of P by WELLORD2:def 1;

assume A2: the InternalRel of P is well-ordering ; :: thesis: for x, y being Element of P st y < x holds

ex z being Element of P st

( z is compact & y <= z & z <= x )

then reconsider L = P as complete Chain by Th9;

let x, y be Element of P; :: thesis: ( y < x implies ex z being Element of P st

( z is compact & y <= z & z <= x ) )

the InternalRel of P, RelIncl (order_type_of the InternalRel of P) are_isomorphic by A2, WELLORD2:def 2;

then consider f being Function such that

A3: f is_isomorphism_of the InternalRel of P, RelIncl (order_type_of the InternalRel of P) ;

assume A4: y < x ; :: thesis: ex z being Element of P st

( z is compact & y <= z & z <= x )

then y <= x ;

then A5: [y,x] in the InternalRel of P ;

then A6: [(f . y),(f . x)] in RelIncl (order_type_of the InternalRel of P) by A3;

then A7: f . x in order_type_of the InternalRel of P by A1, RELAT_1:15;

A8: f . x <> f . y by A3, A4, A5, WELLORD1:36;

A9: f . y in order_type_of the InternalRel of P by A6, A1, RELAT_1:15;

then reconsider a = f . x, b = f . y as Ordinal by A7;

b c= a by A6, A7, A9, WELLORD2:def 1;

then b c< a by A8;

then b in a by ORDINAL1:11;

then A10: succ b c= a by ORDINAL1:21;

then A11: succ b in order_type_of the InternalRel of P by A7, ORDINAL1:12;

then A12: [(succ b),(f . x)] in RelIncl (order_type_of the InternalRel of P) by A7, A10, WELLORD2:def 1;

A13: b c= succ b by ORDINAL3:1;

rng f = order_type_of the InternalRel of P by A3, A1;

then consider z being object such that

A14: z in dom f and

A15: succ b = f . z by A11, FUNCT_1:def 3;

A16: field the InternalRel of P = the carrier of P by ORDERS_1:15;

then reconsider z = z as Element of P by A3, A14;

take z ; :: thesis: ( z is compact & y <= z & z <= x )

A17: dom f = field the InternalRel of P by A3;

thus z is compact :: thesis: ( y <= z & z <= x )

proof

[(f . y),(succ b)] in RelIncl (order_type_of the InternalRel of P)
by A9, A13, A11, WELLORD2:def 1;
let D be non empty directed Subset of P; :: according to WAYBEL_3:def 1,WAYBEL_3:def 2 :: thesis: ( not z <= sup D or ex b_{1} being Element of the carrier of P st

( b_{1} in D & z <= b_{1} ) )

assume that

A18: z <= sup D and

A19: for d being Element of P st d in D holds

not z <= d ; :: thesis: contradiction

A20: L is complete ;

D is_<=_than y

then z <= y by A18, YELLOW_0:def 2;

then [z,y] in the InternalRel of P ;

then [(succ b),b] in RelIncl (order_type_of the InternalRel of P) by A3, A15;

then succ b c= b by A9, A11, WELLORD2:def 1;

then b = succ b by A13;

hence contradiction by ORDINAL1:9; :: thesis: verum

end;( b

assume that

A18: z <= sup D and

A19: for d being Element of P st d in D holds

not z <= d ; :: thesis: contradiction

A20: L is complete ;

D is_<=_than y

proof

then
sup D <= y
by A20, YELLOW_0:32;
let c be Element of P; :: according to LATTICE3:def 9 :: thesis: ( not c in D or c <= y )

A21: f is one-to-one by A3;

assume A22: c in D ; :: thesis: c <= y

then not z <= c by A19;

then z >= c by A20, WAYBEL_0:def 29;

then [c,z] in the InternalRel of P ;

then A23: [(f . c),(succ b)] in RelIncl (order_type_of the InternalRel of P) by A3, A15;

then A24: f . c in order_type_of the InternalRel of P by A1, RELAT_1:15;

then reconsider fc = f . c as Ordinal ;

A25: fc c= succ b by A11, A23, A24, WELLORD2:def 1;

c <> z by A19, A22;

then fc <> succ b by A15, A16, A17, A21, FUNCT_1:def 4;

then fc c< succ b by A25;

then fc in succ b by ORDINAL1:11;

then fc c= b by ORDINAL1:22;

then [fc,b] in RelIncl (order_type_of the InternalRel of P) by A9, A24, WELLORD2:def 1;

hence [c,y] in the InternalRel of P by A3, A16; :: according to ORDERS_2:def 5 :: thesis: verum

end;A21: f is one-to-one by A3;

assume A22: c in D ; :: thesis: c <= y

then not z <= c by A19;

then z >= c by A20, WAYBEL_0:def 29;

then [c,z] in the InternalRel of P ;

then A23: [(f . c),(succ b)] in RelIncl (order_type_of the InternalRel of P) by A3, A15;

then A24: f . c in order_type_of the InternalRel of P by A1, RELAT_1:15;

then reconsider fc = f . c as Ordinal ;

A25: fc c= succ b by A11, A23, A24, WELLORD2:def 1;

c <> z by A19, A22;

then fc <> succ b by A15, A16, A17, A21, FUNCT_1:def 4;

then fc c< succ b by A25;

then fc in succ b by ORDINAL1:11;

then fc c= b by ORDINAL1:22;

then [fc,b] in RelIncl (order_type_of the InternalRel of P) by A9, A24, WELLORD2:def 1;

hence [c,y] in the InternalRel of P by A3, A16; :: according to ORDERS_2:def 5 :: thesis: verum

then z <= y by A18, YELLOW_0:def 2;

then [z,y] in the InternalRel of P ;

then [(succ b),b] in RelIncl (order_type_of the InternalRel of P) by A3, A15;

then succ b c= b by A9, A11, WELLORD2:def 1;

then b = succ b by A13;

hence contradiction by ORDINAL1:9; :: thesis: verum

hence ( [y,z] in the InternalRel of P & [z,x] in the InternalRel of P ) by A3, A15, A16, A12; :: according to ORDERS_2:def 5 :: thesis: verum