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;
assume A1:
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
the InternalRel of P, RelIncl (order_type_of the InternalRel of P) are_isomorphic
by WELLORD2:def 2;
then consider f being Function such that
A2:
f is_isomorphism_of the InternalRel of P, RelIncl (order_type_of the InternalRel of P)
by WELLORD1:def 8;
reconsider L = P as complete Chain by A1, 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 ) )
assume A3:
y < x
; :: thesis: ex z being Element of P st
( z is compact & y <= z & z <= x )
then
( y <= x & y <> x )
by ORDERS_2:def 10;
then
[y,x] in the InternalRel of P
by ORDERS_2:def 9;
then A4:
( [(f . y),(f . x)] in RelIncl (order_type_of the InternalRel of P) & f . x <> f . y )
by A2, A3, WELLORD1:45;
A5:
field (RelIncl (order_type_of the InternalRel of P)) = order_type_of the InternalRel of P
by WELLORD2:def 1;
then A6:
( f . x in order_type_of the InternalRel of P & f . y in order_type_of the InternalRel of P )
by A4, RELAT_1:30;
then reconsider a = f . x, b = f . y as Ordinal ;
b c= a
by A4, A6, WELLORD2:def 1;
then
b c< a
by A4, XBOOLE_0:def 8;
then
b in a
by ORDINAL1:21;
then A7:
( succ b c= a & b c= succ b )
by ORDINAL1:33, ORDINAL3:1;
then A8:
succ b in order_type_of the InternalRel of P
by A6, ORDINAL1:22;
rng f = order_type_of the InternalRel of P
by A2, A5, WELLORD1:def 7;
then consider z being set such that
A9:
( z in dom f & succ b = f . z )
by A8, FUNCT_1:def 5;
A10:
field the InternalRel of P = the carrier of P
by ORDERS_1:100;
A11:
dom f = field the InternalRel of P
by A2, WELLORD1:def 7;
reconsider z = z as Element of P by A2, A9, A10, WELLORD1:def 7;
take
z
; :: thesis: ( z is compact & y <= z & z <= x )
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 <= "\/" D,P or ex b1 being Element of the carrier of P st
( b1 in D & z <= b1 ) )
assume that A12:
z <= sup D
and A13:
for
d being
Element of
P st
d in D holds
not
z <= d
;
:: thesis: contradiction
A14:
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 )
assume A15:
c in D
;
:: thesis: c <= y
then
( not
z <= c &
z <= z )
by A13;
then
z >= c
by A14, WAYBEL_0:def 29;
then
[c,z] in the
InternalRel of
P
by ORDERS_2:def 9;
then A16:
[(f . c),(succ b)] in RelIncl (order_type_of the InternalRel of P)
by A2, A9, WELLORD1:def 7;
then A17:
f . c in order_type_of the
InternalRel of
P
by A5, RELAT_1:30;
then reconsider fc =
f . c as
Ordinal ;
(
c <> z &
f is
one-to-one )
by A2, A13, A15, WELLORD1:def 7;
then
(
fc c= succ b &
fc <> succ b )
by A8, A9, A10, A11, A16, A17, FUNCT_1:def 8, WELLORD2:def 1;
then
fc c< succ b
by XBOOLE_0:def 8;
then
fc in succ b
by ORDINAL1:21;
then
fc c= b
by ORDINAL1:34;
then
[fc,b] in RelIncl (order_type_of the InternalRel of P)
by A6, A17, WELLORD2:def 1;
hence
[c,y] in the
InternalRel of
P
by A2, A10, WELLORD1:def 7;
:: according to ORDERS_2:def 9 :: thesis: verum
end;
then
sup D <= y
by A14, YELLOW_0:32;
then
z <= y
by A12, YELLOW_0:def 2;
then
[z,y] in the
InternalRel of
P
by ORDERS_2:def 9;
then
[(succ b),b] in RelIncl (order_type_of the InternalRel of P)
by A2, A9, WELLORD1:def 7;
then
succ b c= b
by A6, A8, WELLORD2:def 1;
then
b = succ b
by A7, XBOOLE_0:def 10;
hence
contradiction
by ORDINAL1:14;
:: thesis: verum
end;
( [(f . y),(succ b)] in RelIncl (order_type_of the InternalRel of P) & [(succ b),(f . x)] in RelIncl (order_type_of the InternalRel of P) )
by A6, A7, A8, WELLORD2:def 1;
hence
( [y,z] in the InternalRel of P & [z,x] in the InternalRel of P )
by A2, A9, A10, WELLORD1:def 7; :: according to ORDERS_2:def 9 :: thesis: verum