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 )
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 A1: d = sup (SetBelow R,C,d) by Def10;
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;
A2: ex_sup_of H₁(d),L by YELLOW_0:17;
A3: ex_sup_of SetBelow R,C,d,L by YELLOW_0:17;
assume A4: "\/" H₁(d),L <> d ; :: thesis: contradiction
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;

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 A1, A3, 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;
( a in C & [a,d] in R ) by A6, Th18;
hence ex a being Element of L st
( a in C & [a,d] in R & not a <= "\/" H₁(d),L ) by 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
A8: SetBelow R,C,d is_<=_than a and
A9: not "\/" H₁(d),L <= a ;
d <= a by A1, A3, A8, 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 A9, ORDERS_2:def 10; :: thesis: verum

end;

end;

end;

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

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 A10, A13, Th21;
then cc in SupBelow R,C by Def10;
then cc in H₁(d) by A11;
hence contradiction by A2, A12, 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 A1, A3, A11, 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 )
thus A17: cs in C by A15, Th18; :: thesis: ( cc < cs & [cs,d] in R )
not [cs,cc] in R by A16, WAYBEL_4:def 4;
then [cc,cs] in R by A10, A16, A17, 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 A10, A11, 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 A10, 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 A2, YELLOW_4:1;
then cc < "\/" H₁(d),L by A22, ORDERS_2:32;
hence contradiction by A12, ORDERS_2:def 10; :: thesis: verum

end;

end;