let L be non empty complete Poset; :: thesis: 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; :: thesis: 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; :: thesis: R satisfies_SIC_on SupBelow R,C
let c, d be Element of L; :: according to WAYBEL35:def 6 :: thesis: ( 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 ; :: thesis: ex y being Element of L st
( y in SupBelow R,C & [c,y] in R & [y,d] in R & c <> y )
deffunc H₁( Element of L) -> set = { b where b is Element of L : ( b in SupBelow R,C & [b,$1] in R ) } ;
A5: d = "\/" H₁(d),L by A2, Th27;
A6: ex_sup_of H₁(d),L by YELLOW_0:17;
A7: c <= d by A3, WAYBEL_4:def 4;

per cases ( not H₁(d) is_<=_than c or ex g being Element of L st
( H₁(d) is_<=_than g & not c <= g ) ) by A4, A5, A6, YELLOW_0:def 9;

suppose not H₁(d) is_<=_than c ; :: thesis: 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 H₁(d) and
A9: not g <= c by LATTICE3:def 9;
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 ; :: thesis: ( y in SupBelow R,C & [c,y] in R & [y,d] in R & c <> y )
thus y in SupBelow R,C by A11; :: thesis: ( [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 Th25;
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 4; :: thesis: ( [y,d] in R & c <> y )
thus [y,d] in R by A12; :: thesis: c <> y
thus c <> y by A9, A10; :: thesis: verum

end;

suppose ex g being Element of L st
( H₁(d) is_<=_than g & not c <= g ) ; :: thesis: 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
A13: H₁(d) is_<=_than g and
A14: not c <= g ;
d <= g by A5, A6, A13, YELLOW_0:def 9;
hence ex y being Element of L st
( y in SupBelow R,C & [c,y] in R & [y,d] in R & c <> y ) by A7, A14, ORDERS_2:26; :: thesis: verum

end;

end;