let L be non empty Poset; :: thesis:
let R be auxiliary(i) auxiliary(ii) Relation of L; :: thesis:
let C be non empty strict_chain of R; :: thesis:
let X be Subset of C; :: thesis:
assume that
A1: ex_sup_of X,L and
A2: C is maximal ; :: thesis:
set s = "\/" (X,L);
A3: C c= C \/ {("\/" (X,L))} by XBOOLE_1:7;
assume A4: not "\/" (X,L) in C ; :: thesis:
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 )

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 )

let a be Element of L; :: thesis:
assume that
A7: a in C and
A8: not [a,("\/" (X,L))] in R and
A9: not [("\/" (X,L)),a] in R ; :: thesis:
take a ; :: thesis:
thus a in C by A7; :: thesis:
a is_>=_than X

let x be Element of L; :: according to LATTICE3:def 9 :: thesis:
assume A10: x in X ; :: thesis:

per cases in R or [x,a] in R or a = x ) by A7, A10, Def3;

suppose A11: [a,x] in R ; :: thesis:

A12: a <= a ;
x <= "\/" (X,L) by A1, A10, YELLOW_4:1;
hence x <= a by A12, A8, A11, WAYBEL_4:def 4; :: thesis:

end;

suppose ( [x,a] in R or a = x ) ; :: thesis:

hence x <= a by WAYBEL_4:def 3; :: thesis:

end;

end;

end;

then "\/" (X,L) <= a by A1, YELLOW_0:def 9;
hence "\/" (X,L) < a by A4, A7, ORDERS_2:def 6; :: thesis:
thus not [("\/" (X,L)),a] in R by A9; :: thesis:

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 A5, Def3;
reconsider a = a, b = b as Element of L by A13, A14;

per cases by A13, A14, Lm1;

suppose ( a in C & b in C ) ; :: thesis:

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:

end;

suppose ( a in C & b = "\/" (X,L) ) ; :: thesis:

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:

end;

suppose ( a = "\/" (X,L) & b in C ) ; :: thesis:

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:

end;

suppose ( a = "\/" (X,L) & b = "\/" (X,L) ) ; :: thesis:

hence ex cs being Element of L st
( cs in C & "\/" (X,L) < cs & not [("\/" (X,L)),cs] in R ) by A16; :: thesis:

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:
thus ( cs in C & "\/" (X,L) < cs & not [("\/" (X,L)),cs] in R ) by A18, A19, A20; :: thesis:
reconsider cs1 = cs as Element of (subrelstr C) by A18, YELLOW_0:def 15;
take cs1 ; :: thesis:
thus cs = cs1 ; :: thesis:
A21: "\/" (X,L) <= cs by A19, ORDERS_2:def 6;
thus X is_<=_than cs1 :: thesis:

let b be Element of (subrelstr C); :: according to LATTICE3:def 9 :: thesis:
reconsider b0 = b as Element of L by YELLOW_0:58;
assume b in X ; :: thesis:
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:

end;

let a be Element of (subrelstr C); :: thesis:
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:
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: