let L be non empty complete Poset; for R being extra-order Relation of L
for C being satisfying_SIC strict_chain of R holds R satisfies_SIC_on SupBelow (R,C)
let R be extra-order Relation of L; for C being satisfying_SIC strict_chain of R holds R satisfies_SIC_on SupBelow (R,C)
let C be satisfying_SIC strict_chain of R; R satisfies_SIC_on SupBelow (R,C)
let c, d be Element of L; WAYBEL35:def 6 ( c in SupBelow (R,C) & d in SupBelow (R,C) & [c,d] in R & c <> d implies ex y being Element of L st
( y in SupBelow (R,C) & [c,y] in R & [y,d] in R & c <> y ) )
assume that
A1:
c in SupBelow (R,C)
and
A2:
d in SupBelow (R,C)
and
A3:
[c,d] in R
and
A4:
c <> d
; ex y being Element of L st
( y in SupBelow (R,C) & [c,y] in R & [y,d] in R & c <> y )
A5:
c <= d
by A3, WAYBEL_4:def 3;
deffunc H1( Element of L) -> set = { b where b is Element of L : ( b in SupBelow (R,C) & [b,$1] in R ) } ;
A6:
d = "\/" (H1(d),L)
by A2, Th24;
A7:
ex_sup_of H1(d),L
by YELLOW_0:17;
per cases
( not H1(d) is_<=_than c or ex g being Element of L st
( H1(d) is_<=_than g & not c <= g ) )
by A4, A6, A7, YELLOW_0:def 9;
suppose
not
H1(
d)
is_<=_than c
;
ex y being Element of L st
( y in SupBelow (R,C) & [c,y] in R & [y,d] in R & c <> y )then consider g being
Element of
L such that A8:
g in H1(
d)
and A9:
not
g <= c
;
consider y being
Element of
L such that A10:
g = y
and A11:
y in SupBelow (
R,
C)
and A12:
[y,d] in R
by A8;
reconsider y =
y as
Element of
L ;
take
y
;
( y in SupBelow (R,C) & [c,y] in R & [y,d] in R & c <> y )thus
y in SupBelow (
R,
C)
by A11;
( [c,y] in R & [y,d] in R & c <> y )
for
c being
Element of
L holds
ex_sup_of SetBelow (
R,
C,
c),
L
by YELLOW_0:17;
then
SupBelow (
R,
C) is
strict_chain of
R
by Th22;
then
(
[c,y] in R or
c = y or
[y,c] in R )
by A1, A11, Def3;
hence
[c,y] in R
by A9, A10, WAYBEL_4:def 3;
( [y,d] in R & c <> y )thus
[y,d] in R
by A12;
c <> ythus
c <> y
by A9, A10;
verum end;