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 (subrelstr C) st

( cs = cs1 & X is_<=_than cs1 & ( for a being Element of (subrelstr C) 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 (subrelstr C) st

( cs = cs1 & X is_<=_than cs1 & ( for a being Element of (subrelstr C) 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 (subrelstr C) st

( cs = cs1 & X is_<=_than cs1 & ( for a being Element of (subrelstr C) 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 (subrelstr C) st

( cs = cs1 & X is_<=_than cs1 & ( for a being Element of (subrelstr C) 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 (subrelstr C) st

( cs = cs1 & X is_<=_than cs1 & ( for a being Element of (subrelstr C) 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 (subrelstr C) st

( cs = cs1 & X is_<=_than cs1 & ( for a being Element of (subrelstr C) 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 )

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 (subrelstr C) st

( cs = cs1 & X is_<=_than cs1 & ( for a being Element of (subrelstr C) st X is_<=_than a holds

cs1 <= a ) ) )

thus ( cs in C & "\/" (X,L) < cs & not [("\/" (X,L)),cs] in R ) by A18, A19, A20; :: thesis: ex cs1 being Element of (subrelstr C) st

( cs = cs1 & X is_<=_than cs1 & ( for a being Element of (subrelstr C) st X is_<=_than a holds

cs1 <= a ) )

reconsider cs1 = cs as Element of (subrelstr C) by A18, YELLOW_0:def 15;

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

cs1 <= a ) )

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

cs1 <= a ) )

A21: "\/" (X,L) <= cs by A19, ORDERS_2:def 6;

thus X is_<=_than cs1 :: thesis: for a being Element of (subrelstr C) st X is_<=_than a holds

cs1 <= a

reconsider a0 = a as Element of L by YELLOW_0:58;

A22: the carrier of (subrelstr C) = C by YELLOW_0:def 15;

assume X is_<=_than a ; :: thesis: cs1 <= a

then X is_<=_than a0 by A22, YELLOW_0:62;

then A23: "\/" (X,L) <= a0 by A1, YELLOW_0:def 9;

A24: cs <= cs ;

( [cs1,a] in R or a = cs1 or [a,cs1] in R ) by A22, Def3;

then cs <= a0 by A20, A23, A24, WAYBEL_4:def 3, WAYBEL_4:def 4;

hence cs1 <= a by YELLOW_0:60; :: thesis: verum

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 (subrelstr C) st

( cs = cs1 & X is_<=_than cs1 & ( for a being Element of (subrelstr C) 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 (subrelstr C) st

( cs = cs1 & X is_<=_than cs1 & ( for a being Element of (subrelstr C) 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 (subrelstr C) st

( cs = cs1 & X is_<=_than cs1 & ( for a being Element of (subrelstr C) 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 (subrelstr C) st

( cs = cs1 & X is_<=_than cs1 & ( for a being Element of (subrelstr C) 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 (subrelstr C) st

( cs = cs1 & X is_<=_than cs1 & ( for a being Element of (subrelstr C) 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 (subrelstr C) st

( cs = cs1 & X is_<=_than cs1 & ( for a being Element of (subrelstr C) 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

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

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 A5, Def3;

reconsider a = a, b = b as Element of L by A13, A14;

end;ex cs being Element of L st

( cs in C & "\/" (X,L) < cs & not [("\/" (X,L)),cs] in R )

proof

consider a, b being set such that
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

hence "\/" (X,L) < a by A4, A7, ORDERS_2:def 6; :: thesis: not [("\/" (X,L)),a] in R

thus not [("\/" (X,L)),a] in R by A9; :: thesis: verum

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

then
"\/" (X,L) <= a
by A1, YELLOW_0:def 9;
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

end;assume A10: x in X ; :: thesis: x <= a

hence "\/" (X,L) < a by A4, A7, ORDERS_2:def 6; :: thesis: not [("\/" (X,L)),a] in R

thus not [("\/" (X,L)),a] in R by A9; :: thesis: verum

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 A5, Def3;

reconsider a = a, b = b as Element of L by A13, A14;

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 A13, A14, Lm1;

end;

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 )

( 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, A16, A17, Def3; :: thesis: verum

end;( cs in C & "\/" (X,L) < cs & not [("\/" (X,L)),cs] in R ) by A15, A16, A17, Def3; :: thesis: verum

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 )

( 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;( cs in C & "\/" (X,L) < cs & not [("\/" (X,L)),cs] in R ) by A15, A17, A6; :: thesis: verum

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 (subrelstr C) st

( cs = cs1 & X is_<=_than cs1 & ( for a being Element of (subrelstr C) st X is_<=_than a holds

cs1 <= a ) ) )

thus ( cs in C & "\/" (X,L) < cs & not [("\/" (X,L)),cs] in R ) by A18, A19, A20; :: thesis: ex cs1 being Element of (subrelstr C) st

( cs = cs1 & X is_<=_than cs1 & ( for a being Element of (subrelstr C) st X is_<=_than a holds

cs1 <= a ) )

reconsider cs1 = cs as Element of (subrelstr C) by A18, YELLOW_0:def 15;

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

cs1 <= a ) )

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

cs1 <= a ) )

A21: "\/" (X,L) <= cs by A19, ORDERS_2:def 6;

thus X is_<=_than cs1 :: thesis: for a being Element of (subrelstr C) st X is_<=_than a holds

cs1 <= a

proof

let a be Element of (subrelstr C); :: thesis: ( X is_<=_than a implies cs1 <= a )
let b be Element of (subrelstr C); :: 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 A1, YELLOW_4:1;

then b0 <= cs by A21, ORDERS_2:3;

hence b <= cs1 by YELLOW_0:60; :: thesis: verum

end;reconsider b0 = b as Element of L by YELLOW_0:58;

assume b in X ; :: thesis: b <= cs1

then b0 <= "\/" (X,L) by A1, YELLOW_4:1;

then b0 <= cs by A21, ORDERS_2:3;

hence b <= cs1 by YELLOW_0:60; :: thesis: verum

reconsider a0 = a as Element of L by YELLOW_0:58;

A22: the carrier of (subrelstr C) = C by YELLOW_0:def 15;

assume X is_<=_than a ; :: thesis: cs1 <= a

then X is_<=_than a0 by A22, YELLOW_0:62;

then A23: "\/" (X,L) <= a0 by A1, YELLOW_0:def 9;

A24: cs <= cs ;

( [cs1,a] in R or a = cs1 or [a,cs1] in R ) by A22, Def3;

then cs <= a0 by A20, A23, A24, WAYBEL_4:def 3, WAYBEL_4:def 4;

hence cs1 <= a by YELLOW_0:60; :: thesis: verum