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 H1( Element of L) -> set = { b where b is Element of L : ( b in SupBelow (R,C) & [b,\$1] in R ) } ;
set p = "\/" (H1(d),L);
A1: ex_sup_of SetBelow (R,C,d),L by YELLOW_0:17;
A2: H1(d) is_<=_than d
proof
let a be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not a in H1(d) or a <= d )
assume a in H1(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: "\/" (H1(d),L) <> d ; :: thesis: contradiction
ex_sup_of H1(d),L by YELLOW_0:17;
then "\/" (H1(d),L) <= d by ;
then A5: "\/" (H1(d),L) < d by ;
now :: thesis: ex a being Element of L st
( a in C & [a,d] in R & not a <= "\/" (H1(d),L) )
per cases ( not SetBelow (R,C,d) is_<=_than "\/" (H1(d),L) or ex a being Element of L st
( SetBelow (R,C,d) is_<=_than a & not "\/" (H1(d),L) <= a ) )
by ;
suppose not SetBelow (R,C,d) is_<=_than "\/" (H1(d),L) ; :: thesis: ex a being Element of L st
( a in C & [a,d] in R & not a <= "\/" (H1(d),L) )

then consider a being Element of L such that
A6: a in SetBelow (R,C,d) and
A7: not a <= "\/" (H1(d),L) ;
A8: [a,d] in R by ;
a in C by ;
hence ex a being Element of L st
( a in C & [a,d] in R & not a <= "\/" (H1(d),L) ) by A8, A7; :: thesis: verum
end;
suppose ex a being Element of L st
( SetBelow (R,C,d) is_<=_than a & not "\/" (H1(d),L) <= a ) ; :: thesis: ex a being Element of L st
( a in C & [a,d] in R & not a <= "\/" (H1(d),L) )

then consider a being Element of L such that
A9: SetBelow (R,C,d) is_<=_than a and
A10: not "\/" (H1(d),L) <= a ;
d <= a by ;
then "\/" (H1(d),L) < a by ;
hence ex a being Element of L st
( a in C & [a,d] in R & not a <= "\/" (H1(d),L) ) by ; :: 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 <= "\/" (H1(d),L) ;
per cases ( [cc,cc] in R or not [cc,cc] in R ) ;
suppose [cc,cc] in R ; :: thesis: contradiction
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 ;
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 ;
thus cs in C by ; :: thesis: ( cc < cs & [cs,d] in R )
then [cc,cs] in R by ;
then cc <= cs by WAYBEL_4:def 3;
hence cc < cs by ; :: thesis: [cs,d] in R
thus [cs,d] in R by ; :: 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 ;
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 ;
A25: y in SupBelow (R,C) by ;
A26: d <= d ;
y <= cs by ;
then [y,d] in R by ;
then y in H1(d) by A25;
then y <= "\/" (H1(d),L) by ;
then cc < "\/" (H1(d),L) by ;
hence contradiction by A13, ORDERS_2:def 6; :: thesis: verum
end;
end;