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 )

A5: c <= d by ;
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 ;
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 ;
suppose not H1(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 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 ; :: 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 Th22;
then ( [c,y] in R or c = y or [y,c] in R ) by ;
hence [c,y] in R by ; :: thesis: ( [y,d] in R & c <> y )
thus [y,d] in R by A12; :: thesis: c <> y
thus c <> y by ; :: thesis: verum
end;
suppose ex g being Element of L st
( H1(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: H1(d) is_<=_than g and
A14: not c <= g ;
d <= g by ;
hence ex y being Element of L st
( y in SupBelow (R,C) & [c,y] in R & [y,d] in R & c <> y ) by ; :: thesis: verum
end;
end;