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
for d being Element of L st d in SupBelow R,C holds
d = "\/" { b where b is Element of L : ( b in SupBelow R,C & [b,d] in R ) } ,L
let R be extra-order Relation of L; :: thesis: for C being satisfying_SIC strict_chain of R
for d being Element of L st d in SupBelow R,C holds
d = "\/" { b where b is Element of L : ( b in SupBelow R,C & [b,d] in R ) } ,L
let C be satisfying_SIC strict_chain of R; :: thesis: for d being Element of L st d in SupBelow R,C holds
d = "\/" { b where b is Element of L : ( b in SupBelow R,C & [b,d] in R ) } ,L
let d be Element of L; :: thesis: ( d in SupBelow R,C implies d = "\/" { b where b is Element of L : ( b in SupBelow R,C & [b,d] in R ) } ,L )
deffunc H₁( Element of L) -> set = { b where b is Element of L : ( b in SupBelow R,C & [b,$1] in R ) } ;
set p = "\/" H₁(d),L;
A1: ex_sup_of SetBelow R,C,d,L by YELLOW_0:17;
A2: H₁(d) is_<=_than d

proof

let a be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not a in H₁(d) or a <= d )
assume a in H₁(d) ; :: thesis: a <= d
then ex b being Element of L st
( a = b & b in SupBelow R,C & [b,d] in R ) ;
hence a <= d by WAYBEL_4:def 4; :: thesis: verum

end;

assume d in SupBelow R,C ; :: thesis: d = "\/" { b where b is Element of L : ( b in SupBelow R,C & [b,d] in R ) } ,L
then A3: d = sup (SetBelow R,C,d) by Def10;
assume A4: "\/" H₁(d),L <> d ; :: thesis: contradiction
ex_sup_of H₁(d),L by YELLOW_0:17;
then "\/" H₁(d),L <= d by A2, YELLOW_0:def 9;
then A5: "\/" H₁(d),L < d by A4, ORDERS_2:def 10;

now

per cases ( not SetBelow R,C,d is_<=_than "\/" H₁(d),L or ex a being Element of L st
( SetBelow R,C,d is_<=_than a & not "\/" H₁(d),L <= a ) ) by A3, A1, A4, YELLOW_0:def 9;

suppose not SetBelow R,C,d is_<=_than "\/" H₁(d),L ; :: thesis: ex a being Element of L st
( a in C & [a,d] in R & not a <= "\/" H₁(d),L )

then consider a being Element of L such that
A6: a in SetBelow R,C,d and
A7: not a <= "\/" H₁(d),L by LATTICE3:def 9;
A8: [a,d] in R by A6, Th18;
a in C by A6, Th18;
hence ex a being Element of L st
( a in C & [a,d] in R & not a <= "\/" H₁(d),L ) by A8, A7; :: thesis: verum

end;

suppose ex a being Element of L st
( SetBelow R,C,d is_<=_than a & not "\/" H₁(d),L <= a ) ; :: thesis: ex a being Element of L st
( a in C & [a,d] in R & not a <= "\/" H₁(d),L )

then consider a being Element of L such that
A9: SetBelow R,C,d is_<=_than a and
A10: not "\/" H₁(d),L <= a ;
d <= a by A3, A1, A9, YELLOW_0:def 9;
then "\/" H₁(d),L < a by A5, ORDERS_2:32;
hence ex a being Element of L st
( a in C & [a,d] in R & not a <= "\/" H₁(d),L ) by A10, ORDERS_2:def 10; :: thesis: verum

end;

end;

end;

then consider cc being Element of L such that
A11: cc in C and
A12: [cc,d] in R and
A13: not cc <= "\/" H₁(d),L ;

per cases ( [cc,cc] in R or not [cc,cc] in R ) ;

suppose [cc,cc] in R ; :: thesis: contradiction

then cc = sup (SetBelow R,C,cc) by A11, YELLOW_0:17, Th21;
then cc in SupBelow R,C by Def10;
then cc in H₁(d) by A12;
hence contradiction by YELLOW_0:17, A13, YELLOW_4:1; :: thesis: verum

end;

suppose A14: not [cc,cc] in R ; :: thesis: contradiction

ex cs being Element of L st
( cs in C & cc < cs & [cs,d] in R )

proof

per cases ( not SetBelow R,C,d is_<=_than cc or ex a being Element of L st
( SetBelow R,C,d is_<=_than a & not cc <= a ) ) by A3, A1, A12, A14, YELLOW_0:def 9;

suppose not SetBelow R,C,d is_<=_than cc ; :: thesis: ex cs being Element of L st
( cs in C & cc < cs & [cs,d] in R )

then consider cs being Element of L such that
A15: cs in SetBelow R,C,d and
A16: not cs <= cc by LATTICE3:def 9;
take cs ; :: thesis: ( cs in C & cc < cs & [cs,d] in R )
A17: not [cs,cc] in R by A16, WAYBEL_4:def 4;
thus cs in C by A15, Th18; :: thesis: ( cc < cs & [cs,d] in R )
then [cc,cs] in R by A17, A11, A16, Def3;
then cc <= cs by WAYBEL_4:def 4;
hence cc < cs by A16, ORDERS_2:def 10; :: thesis: [cs,d] in R
thus [cs,d] in R by A15, Th18; :: thesis: verum

end;

suppose A18: ex a being Element of L st
( SetBelow R,C,d is_<=_than a & not cc <= a ) ; :: thesis: ex cs being Element of L st
( cs in C & cc < cs & [cs,d] in R )

cc in SetBelow R,C,d by A11, A12, Th18;
hence ex cs being Element of L st
( cs in C & cc < cs & [cs,d] in R ) by A18, LATTICE3:def 9; :: thesis: verum

end;

end;

end;

then consider cs being Element of L such that
A19: cs in C and
A20: cc < cs and
A21: [cs,d] in R ;
consider y being Element of L such that
A22: cc < y and
A23: [y,cs] in R and
A24: y = sup (SetBelow R,C,y) by A11, A19, A20, Th22;
A25: y in SupBelow R,C by A24, Def10;
A26: d <= d ;
y <= cs by A23, WAYBEL_4:def 4;
then [y,d] in R by A21, A26, WAYBEL_4:def 5;
then y in H₁(d) by A25;
then y <= "\/" H₁(d),L by YELLOW_0:17, YELLOW_4:1;
then cc < "\/" H₁(d),L by A22, ORDERS_2:32;
hence contradiction by A13, ORDERS_2:def 10; :: thesis: verum

end;

end;