let L be non empty lower-bounded Poset; :: thesis: for R being extra-order Relation of L

for C being non empty strict_chain of R st C is sup-closed & ( for c being Element of L st c in C holds

ex_sup_of SetBelow (R,C,c),L ) & R satisfies_SIC_on C holds

for c being Element of L st c in C holds

c = sup (SetBelow (R,C,c))

let R be extra-order Relation of L; :: thesis: for C being non empty strict_chain of R st C is sup-closed & ( for c being Element of L st c in C holds

ex_sup_of SetBelow (R,C,c),L ) & R satisfies_SIC_on C holds

for c being Element of L st c in C holds

c = sup (SetBelow (R,C,c))

let C be non empty strict_chain of R; :: thesis: ( C is sup-closed & ( for c being Element of L st c in C holds

ex_sup_of SetBelow (R,C,c),L ) & R satisfies_SIC_on C implies for c being Element of L st c in C holds

c = sup (SetBelow (R,C,c)) )

assume that

A1: C is sup-closed and

A2: for c being Element of L st c in C holds

ex_sup_of SetBelow (R,C,c),L ; :: thesis: ( not R satisfies_SIC_on C or for c being Element of L st c in C holds

c = sup (SetBelow (R,C,c)) )

assume A3: R satisfies_SIC_on C ; :: thesis: for c being Element of L st c in C holds

c = sup (SetBelow (R,C,c))

let c be Element of L; :: thesis: ( c in C implies c = sup (SetBelow (R,C,c)) )

assume A4: c in C ; :: thesis: c = sup (SetBelow (R,C,c))

A5: ex_sup_of SetBelow (R,C,c),L by A2, A4;

set d = sup (SetBelow (R,C,c));

SetBelow (R,C,c) c= C by XBOOLE_1:17;

then sup (SetBelow (R,C,c)) = "\/" ((SetBelow (R,C,c)),(subrelstr C)) by A1, A5;

then sup (SetBelow (R,C,c)) in the carrier of (subrelstr C) ;

then A6: sup (SetBelow (R,C,c)) in C by YELLOW_0:def 15;

for C being non empty strict_chain of R st C is sup-closed & ( for c being Element of L st c in C holds

ex_sup_of SetBelow (R,C,c),L ) & R satisfies_SIC_on C holds

for c being Element of L st c in C holds

c = sup (SetBelow (R,C,c))

let R be extra-order Relation of L; :: thesis: for C being non empty strict_chain of R st C is sup-closed & ( for c being Element of L st c in C holds

ex_sup_of SetBelow (R,C,c),L ) & R satisfies_SIC_on C holds

for c being Element of L st c in C holds

c = sup (SetBelow (R,C,c))

let C be non empty strict_chain of R; :: thesis: ( C is sup-closed & ( for c being Element of L st c in C holds

ex_sup_of SetBelow (R,C,c),L ) & R satisfies_SIC_on C implies for c being Element of L st c in C holds

c = sup (SetBelow (R,C,c)) )

assume that

A1: C is sup-closed and

A2: for c being Element of L st c in C holds

ex_sup_of SetBelow (R,C,c),L ; :: thesis: ( not R satisfies_SIC_on C or for c being Element of L st c in C holds

c = sup (SetBelow (R,C,c)) )

assume A3: R satisfies_SIC_on C ; :: thesis: for c being Element of L st c in C holds

c = sup (SetBelow (R,C,c))

let c be Element of L; :: thesis: ( c in C implies c = sup (SetBelow (R,C,c)) )

assume A4: c in C ; :: thesis: c = sup (SetBelow (R,C,c))

A5: ex_sup_of SetBelow (R,C,c),L by A2, A4;

set d = sup (SetBelow (R,C,c));

SetBelow (R,C,c) c= C by XBOOLE_1:17;

then sup (SetBelow (R,C,c)) = "\/" ((SetBelow (R,C,c)),(subrelstr C)) by A1, A5;

then sup (SetBelow (R,C,c)) in the carrier of (subrelstr C) ;

then A6: sup (SetBelow (R,C,c)) in C by YELLOW_0:def 15;

per cases
( c = sup (SetBelow (R,C,c)) or c <> sup (SetBelow (R,C,c)) )
;

end;

suppose A7:
c <> sup (SetBelow (R,C,c))
; :: thesis: c = sup (SetBelow (R,C,c))

then ( c <= sup (SetBelow (R,C,c)) or [(sup (SetBelow (R,C,c))),c] in R ) by WAYBEL_4:def 3;

then consider y being Element of L such that

A12: y in C and

[(sup (SetBelow (R,C,c))),y] in R and

A13: [y,c] in R and

A14: sup (SetBelow (R,C,c)) < y by A8, A3, A4, A6, A7, Th13, ORDERS_2:def 6;

y in SetBelow (R,C,c) by A12, A13, Th15;

hence c = sup (SetBelow (R,C,c)) by A5, A14, ORDERS_2:6, YELLOW_4:1; :: thesis: verum

end;

A8: now :: thesis: ( c < sup (SetBelow (R,C,c)) implies c = sup (SetBelow (R,C,c)) )

( [c,(sup (SetBelow (R,C,c)))] in R or [(sup (SetBelow (R,C,c))),c] in R )
by A7, A4, A6, Def3;assume A9:
c < sup (SetBelow (R,C,c))
; :: thesis: c = sup (SetBelow (R,C,c))

A10: for a being Element of L st SetBelow (R,C,c) is_<=_than a holds

c <= a

hence c = sup (SetBelow (R,C,c)) by A10, A5, YELLOW_0:def 9; :: thesis: verum

end;A10: for a being Element of L st SetBelow (R,C,c) is_<=_than a holds

c <= a

proof

SetBelow (R,C,c) is_<=_than c
by Th16;
let a be Element of L; :: thesis: ( SetBelow (R,C,c) is_<=_than a implies c <= a )

assume SetBelow (R,C,c) is_<=_than a ; :: thesis: c <= a

then A11: sup (SetBelow (R,C,c)) <= a by A5, YELLOW_0:def 9;

c <= sup (SetBelow (R,C,c)) by A9, ORDERS_2:def 6;

hence c <= a by A11, ORDERS_2:3; :: thesis: verum

end;assume SetBelow (R,C,c) is_<=_than a ; :: thesis: c <= a

then A11: sup (SetBelow (R,C,c)) <= a by A5, YELLOW_0:def 9;

c <= sup (SetBelow (R,C,c)) by A9, ORDERS_2:def 6;

hence c <= a by A11, ORDERS_2:3; :: thesis: verum

hence c = sup (SetBelow (R,C,c)) by A10, A5, YELLOW_0:def 9; :: thesis: verum

then ( c <= sup (SetBelow (R,C,c)) or [(sup (SetBelow (R,C,c))),c] in R ) by WAYBEL_4:def 3;

then consider y being Element of L such that

A12: y in C and

[(sup (SetBelow (R,C,c))),y] in R and

A13: [y,c] in R and

A14: sup (SetBelow (R,C,c)) < y by A8, A3, A4, A6, A7, Th13, ORDERS_2:def 6;

y in SetBelow (R,C,c) by A12, A13, Th15;

hence c = sup (SetBelow (R,C,c)) by A5, A14, ORDERS_2:6, YELLOW_4:1; :: thesis: verum