let L be non empty complete Poset; for R being extra-order Relation of L
for C being satisfying_SIC strict_chain of R
for d being Element of L st d in SupBelow (R,C) holds
d = "\/" ( { b where b is Element of L : ( b in SupBelow (R,C) & [b,d] in R ) } ,L)
let R be extra-order Relation of L; for C being satisfying_SIC strict_chain of R
for d being Element of L st d in SupBelow (R,C) holds
d = "\/" ( { b where b is Element of L : ( b in SupBelow (R,C) & [b,d] in R ) } ,L)
let C be satisfying_SIC strict_chain of R; for d being Element of L st d in SupBelow (R,C) holds
d = "\/" ( { b where b is Element of L : ( b in SupBelow (R,C) & [b,d] in R ) } ,L)
let d be Element of L; ( d in SupBelow (R,C) implies d = "\/" ( { b where b is Element of L : ( b in SupBelow (R,C) & [b,d] in R ) } ,L) )
deffunc H1( Element of L) -> set = { b where b is Element of L : ( b in SupBelow (R,C) & [b,$1] in R ) } ;
set p = "\/" (H1(d),L);
A1:
ex_sup_of SetBelow (R,C,d),L
by YELLOW_0:17;
A2:
H1(d) is_<=_than d
assume
d in SupBelow (R,C)
; d = "\/" ( { b where b is Element of L : ( b in SupBelow (R,C) & [b,d] in R ) } ,L)
then A3:
d = sup (SetBelow (R,C,d))
by Def10;
assume A4:
"\/" (H1(d),L) <> d
; contradiction
ex_sup_of H1(d),L
by YELLOW_0:17;
then
"\/" (H1(d),L) <= d
by A2, YELLOW_0:def 9;
then A5:
"\/" (H1(d),L) < d
by A4, ORDERS_2:def 6;
now ex a being Element of L st
( a in C & [a,d] in R & not a <= "\/" (H1(d),L) )per cases
( not SetBelow (R,C,d) is_<=_than "\/" (H1(d),L) or ex a being Element of L st
( SetBelow (R,C,d) is_<=_than a & not "\/" (H1(d),L) <= a ) )
by A3, A1, A4, YELLOW_0:def 9;
suppose
ex
a being
Element of
L st
(
SetBelow (
R,
C,
d)
is_<=_than a & not
"\/" (
H1(
d),
L)
<= a )
;
ex a being Element of L st
( a in C & [a,d] in R & not a <= "\/" (H1(d),L) )then consider a being
Element of
L such that A9:
SetBelow (
R,
C,
d)
is_<=_than a
and A10:
not
"\/" (
H1(
d),
L)
<= a
;
d <= a
by A3, A1, A9, YELLOW_0:def 9;
then
"\/" (
H1(
d),
L)
< a
by A5, ORDERS_2:7;
hence
ex
a being
Element of
L st
(
a in C &
[a,d] in R & not
a <= "\/" (
H1(
d),
L) )
by A10, ORDERS_2:def 6;
verum end; end; end;
then consider cc being Element of L such that
A11:
cc in C
and
A12:
[cc,d] in R
and
A13:
not cc <= "\/" (H1(d),L)
;
per cases
( [cc,cc] in R or not [cc,cc] in R )
;
suppose A14:
not
[cc,cc] in R
;
contradiction
ex
cs being
Element of
L st
(
cs in C &
cc < cs &
[cs,d] in R )
proof
per cases
( not SetBelow (R,C,d) is_<=_than cc or ex a being Element of L st
( SetBelow (R,C,d) is_<=_than a & not cc <= a ) )
by A3, A1, A12, A14, YELLOW_0:def 9;
suppose
not
SetBelow (
R,
C,
d)
is_<=_than cc
;
ex cs being Element of L st
( cs in C & cc < cs & [cs,d] in R )then consider cs being
Element of
L such that A15:
cs in SetBelow (
R,
C,
d)
and A16:
not
cs <= cc
;
take
cs
;
( cs in C & cc < cs & [cs,d] in R )A17:
not
[cs,cc] in R
by A16, WAYBEL_4:def 3;
thus
cs in C
by A15, Th15;
( cc < cs & [cs,d] in R )then
[cc,cs] in R
by A17, A11, A16, Def3;
then
cc <= cs
by WAYBEL_4:def 3;
hence
cc < cs
by A16, ORDERS_2:def 6;
[cs,d] in Rthus
[cs,d] in R
by A15, Th15;
verum end; end;
end; then consider cs being
Element of
L such that A19:
cs in C
and A20:
cc < cs
and A21:
[cs,d] in R
;
consider y being
Element of
L such that A22:
cc < y
and A23:
[y,cs] in R
and A24:
y = sup (SetBelow (R,C,y))
by A11, A19, A20, Th19;
A25:
y in SupBelow (
R,
C)
by A24, Def10;
A26:
d <= d
;
y <= cs
by A23, WAYBEL_4:def 3;
then
[y,d] in R
by A21, A26, WAYBEL_4:def 4;
then
y in H1(
d)
by A25;
then
y <= "\/" (
H1(
d),
L)
by YELLOW_0:17, YELLOW_4:1;
then
cc < "\/" (
H1(
d),
L)
by A22, ORDERS_2:7;
hence
contradiction
by A13, ORDERS_2:def 6;
verum end; end;