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 ;
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 ;
A8: f . x <> f . y by ;
A9: f . y in order_type_of the InternalRel of P by ;
then reconsider a = f . x, b = f . y as Ordinal by A7;
b c= a by ;
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 ;
then A12: [(succ b),(f . x)] in RelIncl (order_type_of the InternalRel of P) by ;
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 ;
A16: field the InternalRel of P = the carrier of P by ORDERS_1:15;
then reconsider z = z as Element of P by ;
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
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 b1 being Element of the carrier of P st
( b1 in D & z <= b1 ) )

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
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 ;
then [c,z] in the InternalRel of P ;
then A23: [(f . c),(succ b)] in RelIncl (order_type_of the InternalRel of P) by ;
then A24: f . c in order_type_of the InternalRel of P by ;
then reconsider fc = f . c as Ordinal ;
A25: fc c= succ b by ;
c <> z by ;
then fc <> succ b by ;
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 ;
hence [c,y] in the InternalRel of P by ; :: according to ORDERS_2:def 5 :: thesis: verum
end;
then sup D <= y by ;
then z <= y by ;
then [z,y] in the InternalRel of P ;
then [(succ b),b] in RelIncl (order_type_of the InternalRel of P) by ;
then succ b c= b by ;
then b = succ b by A13;
hence contradiction by ORDINAL1:9; :: thesis: verum
end;
[(f . y),(succ b)] in RelIncl (order_type_of the InternalRel of P) by ;
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