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 3; :: 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 6;

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

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) ;
A8: [a,d] in R by A6, Th15;
a in C by A6, Th15;
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:7;
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 6; :: 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, Th18, YELLOW_0:17;
then cc in SupBelow (R,C) by Def10;
then cc in H₁(d) by A12;
hence contradiction by A13, YELLOW_0:17, 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 ;
take cs ; :: thesis: ( cs in C & cc < cs & [cs,d] in R )
A17: not [cs,cc] in R by A16, WAYBEL_4:def 3;
thus cs in C by A15, Th15; :: thesis: ( cc < cs & [cs,d] in R )
then [cc,cs] in R by A17, A11, A16, Def3;
then cc <= cs by WAYBEL_4:def 3;
hence cc < cs by A16, ORDERS_2:def 6; :: thesis: [cs,d] in R
thus [cs,d] in R by A15, Th15; :: 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, Th15;
hence ex cs being Element of L st
( cs in C & cc < cs & [cs,d] in R ) by A18; :: 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, Th19;
A25: y in SupBelow (R,C) by A24, Def10;
A26: d <= d ;
y <= cs by A23, WAYBEL_4:def 3;
then [y,d] in R by A21, A26, WAYBEL_4:def 4;
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:7;
hence contradiction by A13, ORDERS_2:def 6; :: thesis: verum

end;

end;