let P be non empty upper-bounded Poset; ( 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
; 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; ( 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
; 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
; ( z is compact & y <= z & z <= x )
A17:
dom f = field the InternalRel of P
by A3;
thus
z is compact
( y <= z & z <= x )proof
let D be non
empty directed Subset of
P;
WAYBEL_3:def 1,
WAYBEL_3:def 2 ( 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
;
contradiction
A20:
L is
complete
;
D is_<=_than y
proof
let c be
Element of
P;
LATTICE3:def 9 ( not c in D or c <= y )
A21:
f is
one-to-one
by A3;
assume A22:
c in D
;
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;
ORDERS_2:def 5 verum
end;
then
sup D <= y
by A20, YELLOW_0:32;
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;
verum
end;
[(f . y),(succ b)] in RelIncl (order_type_of the InternalRel of P)
by A9, A13, A11, WELLORD2:def 1;
hence
( [y,z] in the InternalRel of P & [z,x] in the InternalRel of P )
by A3, A15, A16, A12; ORDERS_2:def 5 verum