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_{1}( Element of L) -> set = { b where b is Element of L : ( b in SupBelow (R,C) & [b,$1] in R ) } ;

set p = "\/" (H_{1}(d),L);

A1: ex_sup_of SetBelow (R,C,d),L by YELLOW_0:17;

A2: H_{1}(d) is_<=_than d

then A3: d = sup (SetBelow (R,C,d)) by Def10;

assume A4: "\/" (H_{1}(d),L) <> d
; :: thesis: contradiction

ex_sup_of H_{1}(d),L
by YELLOW_0:17;

then "\/" (H_{1}(d),L) <= d
by A2, YELLOW_0:def 9;

then A5: "\/" (H_{1}(d),L) < d
by A4, ORDERS_2:def 6;

A11: cc in C and

A12: [cc,d] in R and

A13: not cc <= "\/" (H_{1}(d),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

set p = "\/" (H

A1: ex_sup_of SetBelow (R,C,d),L by YELLOW_0:17;

A2: H

proof

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)
let a be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not a in H_{1}(d) or a <= d )

assume a in H_{1}(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 a in H

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

then A3: d = sup (SetBelow (R,C,d)) by Def10;

assume A4: "\/" (H

ex_sup_of H

then "\/" (H

then A5: "\/" (H

now :: thesis: ex a being Element of L st

( a in C & [a,d] in R & not a <= "\/" (H_{1}(d),L) )end;

then consider cc being Element of L such that ( a in C & [a,d] in R & not a <= "\/" (H

per cases
( not SetBelow (R,C,d) is_<=_than "\/" (H_{1}(d),L) or ex a being Element of L st

( SetBelow (R,C,d) is_<=_than a & not "\/" (H_{1}(d),L) <= a ) )
by A3, A1, A4, YELLOW_0:def 9;

end;

( SetBelow (R,C,d) is_<=_than a & not "\/" (H

suppose
not SetBelow (R,C,d) is_<=_than "\/" (H_{1}(d),L)
; :: thesis: ex a being Element of L st

( a in C & [a,d] in R & not a <= "\/" (H_{1}(d),L) )

( a in C & [a,d] in R & not a <= "\/" (H

then consider a being Element of L such that

A6: a in SetBelow (R,C,d) and

A7: not a <= "\/" (H_{1}(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_{1}(d),L) )
by A8, A7; :: thesis: verum

end;A6: a in SetBelow (R,C,d) and

A7: not a <= "\/" (H

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

suppose
ex a being Element of L st

( SetBelow (R,C,d) is_<=_than a & not "\/" (H_{1}(d),L) <= a )
; :: thesis: ex a being Element of L st

( a in C & [a,d] in R & not a <= "\/" (H_{1}(d),L) )

( SetBelow (R,C,d) is_<=_than a & not "\/" (H

( a in C & [a,d] in R & not a <= "\/" (H

then consider a being Element of L such that

A9: SetBelow (R,C,d) is_<=_than a and

A10: not "\/" (H_{1}(d),L) <= a
;

d <= a by A3, A1, A9, YELLOW_0:def 9;

then "\/" (H_{1}(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_{1}(d),L) )
by A10, ORDERS_2:def 6; :: thesis: verum

end;A9: SetBelow (R,C,d) is_<=_than a and

A10: not "\/" (H

d <= a by A3, A1, A9, YELLOW_0:def 9;

then "\/" (H

hence ex a being Element of L st

( a in C & [a,d] in R & not a <= "\/" (H

A11: cc in C and

A12: [cc,d] in R and

A13: not cc <= "\/" (H

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

end;

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_{1}(d)
by A12;

hence contradiction by A13, YELLOW_0:17, YELLOW_4:1; :: thesis: verum

end;then cc in SupBelow (R,C) by Def10;

then cc in H

hence contradiction by A13, YELLOW_0:17, YELLOW_4:1; :: thesis: verum

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 )

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_{1}(d)
by A25;

then y <= "\/" (H_{1}(d),L)
by YELLOW_0:17, YELLOW_4:1;

then cc < "\/" (H_{1}(d),L)
by A22, ORDERS_2:7;

hence contradiction by A13, ORDERS_2:def 6; :: thesis: verum

end;( cs in C & cc < cs & [cs,d] in R )

proof
end;

then consider cs being Element of L such that 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;

end;

( 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 )

( 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;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

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 )

( 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;hence ex cs being Element of L st

( cs in C & cc < cs & [cs,d] in R ) by A18; :: thesis: verum

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

then y <= "\/" (H

then cc < "\/" (H

hence contradiction by A13, ORDERS_2:def 6; :: thesis: verum