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_{1}( Element of L) -> set = { b where b is Element of L : ( b in SupBelow (R,C) & [b,$1] in R ) } ;

A6: d = "\/" (H_{1}(d),L)
by A2, Th24;

A7: ex_sup_of H_{1}(d),L
by YELLOW_0:17;

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

A6: d = "\/" (H

A7: ex_sup_of H

per cases
( not H_{1}(d) is_<=_than c or ex g being Element of L st

( H_{1}(d) is_<=_than g & not c <= g ) )
by A4, A6, A7, YELLOW_0:def 9;

end;

( H

suppose
not H_{1}(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 )

( 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_{1}(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;A8: g in H

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

suppose
ex g being Element of L st

( H_{1}(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 )

( H

( 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_{1}(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;A13: H

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