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 A3, WAYBEL_4:def 3;
deffunc H₁( Element of L) -> set = { b where b is Element of L : ( b in SupBelow (R,C) & [b,$1] in R ) } ;
A6: d = "\/" (H₁(d),L) by A2, Th24;
A7: ex_sup_of H₁(d),L by YELLOW_0:17;

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, A6, A7, 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 ;
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 A1, A11, Def3;
hence [c,y] in R by A9, A10, WAYBEL_4:def 3; :: 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 A6, A7, 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 A5, A14, ORDERS_2:3; :: thesis: verum

end;

end;