let L be non empty Poset; :: thesis: for R being auxiliary(i) auxiliary(ii) Relation of L
for C being non empty strict_chain of R
for X being Subset of C st ex_sup_of X,L & C is maximal & not "\/" (X,L) in C holds
ex cs being Element of L st
( cs in C & "\/" (X,L) < cs & not [("\/" (X,L)),cs] in R & ex cs1 being Element of () st
( cs = cs1 & X is_<=_than cs1 & ( for a being Element of () st X is_<=_than a holds
cs1 <= a ) ) )

let R be auxiliary(i) auxiliary(ii) Relation of L; :: thesis: for C being non empty strict_chain of R
for X being Subset of C st ex_sup_of X,L & C is maximal & not "\/" (X,L) in C holds
ex cs being Element of L st
( cs in C & "\/" (X,L) < cs & not [("\/" (X,L)),cs] in R & ex cs1 being Element of () st
( cs = cs1 & X is_<=_than cs1 & ( for a being Element of () st X is_<=_than a holds
cs1 <= a ) ) )

let C be non empty strict_chain of R; :: thesis: for X being Subset of C st ex_sup_of X,L & C is maximal & not "\/" (X,L) in C holds
ex cs being Element of L st
( cs in C & "\/" (X,L) < cs & not [("\/" (X,L)),cs] in R & ex cs1 being Element of () st
( cs = cs1 & X is_<=_than cs1 & ( for a being Element of () st X is_<=_than a holds
cs1 <= a ) ) )

let X be Subset of C; :: thesis: ( ex_sup_of X,L & C is maximal & not "\/" (X,L) in C implies ex cs being Element of L st
( cs in C & "\/" (X,L) < cs & not [("\/" (X,L)),cs] in R & ex cs1 being Element of () st
( cs = cs1 & X is_<=_than cs1 & ( for a being Element of () st X is_<=_than a holds
cs1 <= a ) ) ) )

assume that
A1: ex_sup_of X,L and
A2: C is maximal ; :: thesis: ( "\/" (X,L) in C or ex cs being Element of L st
( cs in C & "\/" (X,L) < cs & not [("\/" (X,L)),cs] in R & ex cs1 being Element of () st
( cs = cs1 & X is_<=_than cs1 & ( for a being Element of () st X is_<=_than a holds
cs1 <= a ) ) ) )

set s = "\/" (X,L);
A3: C c= C \/ {("\/" (X,L))} by XBOOLE_1:7;
assume A4: not "\/" (X,L) in C ; :: thesis: ex cs being Element of L st
( cs in C & "\/" (X,L) < cs & not [("\/" (X,L)),cs] in R & ex cs1 being Element of () st
( cs = cs1 & X is_<=_than cs1 & ( for a being Element of () st X is_<=_than a holds
cs1 <= a ) ) )

then not C \/ {("\/" (X,L))} c= C by ZFMISC_1:39;
then A5: C \/ {("\/" (X,L))} is not strict_chain of R by A3, A2;
ex cs being Element of L st
( cs in C & "\/" (X,L) < cs & not [("\/" (X,L)),cs] in R )
proof
A6: for a being Element of L st a in C & not [a,("\/" (X,L))] in R & not [("\/" (X,L)),a] in R holds
ex cs being Element of L st
( cs in C & "\/" (X,L) < cs & not [("\/" (X,L)),cs] in R )
proof
let a be Element of L; :: thesis: ( a in C & not [a,("\/" (X,L))] in R & not [("\/" (X,L)),a] in R implies ex cs being Element of L st
( cs in C & "\/" (X,L) < cs & not [("\/" (X,L)),cs] in R ) )

assume that
A7: a in C and
A8: not [a,("\/" (X,L))] in R and
A9: not [("\/" (X,L)),a] in R ; :: thesis: ex cs being Element of L st
( cs in C & "\/" (X,L) < cs & not [("\/" (X,L)),cs] in R )

take a ; :: thesis: ( a in C & "\/" (X,L) < a & not [("\/" (X,L)),a] in R )
thus a in C by A7; :: thesis: ( "\/" (X,L) < a & not [("\/" (X,L)),a] in R )
a is_>=_than X
proof
let x be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not x in X or x <= a )
assume A10: x in X ; :: thesis: x <= a
per cases ( [a,x] in R or [x,a] in R or a = x ) by ;
suppose A11: [a,x] in R ; :: thesis: x <= a
A12: a <= a ;
x <= "\/" (X,L) by ;
hence x <= a by ; :: thesis: verum
end;
suppose ( [x,a] in R or a = x ) ; :: thesis: x <= a
end;
end;
end;
then "\/" (X,L) <= a by ;
hence "\/" (X,L) < a by ; :: thesis: not [("\/" (X,L)),a] in R
thus not [("\/" (X,L)),a] in R by A9; :: thesis: verum
end;
consider a, b being set such that
A13: a in C \/ {("\/" (X,L))} and
A14: b in C \/ {("\/" (X,L))} and
A15: not [a,b] in R and
A16: a <> b and
A17: not [b,a] in R by ;
reconsider a = a, b = b as Element of L by ;
per cases ( ( a in C & b in C ) or ( a in C & b = "\/" (X,L) ) or ( a = "\/" (X,L) & b in C ) or ( a = "\/" (X,L) & b = "\/" (X,L) ) ) by ;
suppose ( a in C & b in C ) ; :: thesis: ex cs being Element of L st
( cs in C & "\/" (X,L) < cs & not [("\/" (X,L)),cs] in R )

hence ex cs being Element of L st
( cs in C & "\/" (X,L) < cs & not [("\/" (X,L)),cs] in R ) by ; :: thesis: verum
end;
suppose ( a in C & b = "\/" (X,L) ) ; :: thesis: ex cs being Element of L st
( cs in C & "\/" (X,L) < cs & not [("\/" (X,L)),cs] in R )

hence ex cs being Element of L st
( cs in C & "\/" (X,L) < cs & not [("\/" (X,L)),cs] in R ) by A15, A17, A6; :: thesis: verum
end;
suppose ( a = "\/" (X,L) & b in C ) ; :: thesis: ex cs being Element of L st
( cs in C & "\/" (X,L) < cs & not [("\/" (X,L)),cs] in R )

hence ex cs being Element of L st
( cs in C & "\/" (X,L) < cs & not [("\/" (X,L)),cs] in R ) by A15, A17, A6; :: thesis: verum
end;
suppose ( a = "\/" (X,L) & b = "\/" (X,L) ) ; :: thesis: ex cs being Element of L st
( cs in C & "\/" (X,L) < cs & not [("\/" (X,L)),cs] in R )

hence ex cs being Element of L st
( cs in C & "\/" (X,L) < cs & not [("\/" (X,L)),cs] in R ) by A16; :: thesis: verum
end;
end;
end;
then consider cs being Element of L such that
A18: cs in C and
A19: "\/" (X,L) < cs and
A20: not [("\/" (X,L)),cs] in R ;
take cs ; :: thesis: ( cs in C & "\/" (X,L) < cs & not [("\/" (X,L)),cs] in R & ex cs1 being Element of () st
( cs = cs1 & X is_<=_than cs1 & ( for a being Element of () st X is_<=_than a holds
cs1 <= a ) ) )

thus ( cs in C & "\/" (X,L) < cs & not [("\/" (X,L)),cs] in R ) by ; :: thesis: ex cs1 being Element of () st
( cs = cs1 & X is_<=_than cs1 & ( for a being Element of () st X is_<=_than a holds
cs1 <= a ) )

reconsider cs1 = cs as Element of () by ;
take cs1 ; :: thesis: ( cs = cs1 & X is_<=_than cs1 & ( for a being Element of () st X is_<=_than a holds
cs1 <= a ) )

thus cs = cs1 ; :: thesis: ( X is_<=_than cs1 & ( for a being Element of () st X is_<=_than a holds
cs1 <= a ) )

A21: "\/" (X,L) <= cs by ;
thus X is_<=_than cs1 :: thesis: for a being Element of () st X is_<=_than a holds
cs1 <= a
proof
let b be Element of (); :: according to LATTICE3:def 9 :: thesis: ( not b in X or b <= cs1 )
reconsider b0 = b as Element of L by YELLOW_0:58;
assume b in X ; :: thesis: b <= cs1
then b0 <= "\/" (X,L) by ;
then b0 <= cs by ;
hence b <= cs1 by YELLOW_0:60; :: thesis: verum
end;
let a be Element of (); :: thesis: ( X is_<=_than a implies cs1 <= a )
reconsider a0 = a as Element of L by YELLOW_0:58;
A22: the carrier of () = C by YELLOW_0:def 15;
assume X is_<=_than a ; :: thesis: cs1 <= a
then X is_<=_than a0 by ;
then A23: "\/" (X,L) <= a0 by ;
A24: cs <= cs ;
( [cs1,a] in R or a = cs1 or [a,cs1] in R ) by ;
then cs <= a0 by ;
hence cs1 <= a by YELLOW_0:60; :: thesis: verum