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;
assume A3: not "\/" X,L in C ; :: thesis:
then A4: not C \/ {("\/" X,L)} c= C by ZFMISC_1:45;
C c= C \/ {("\/" X,L)} by XBOOLE_1:7;
then A5: C \/ {("\/" X,L)} is not strict_chain of R by A2, A4, Def4;
ex cs being Element of L st
( cs in C & "\/" X,L < cs & not [("\/" X,L),cs] in R )

consider a, b being set such that
A6: a in C \/ {("\/" X,L)} and
A7: b in C \/ {("\/" X,L)} and
A8: not [a,b] in R and
A9: a <> b and
A10: not [b,a] in R by A5, Def3;
reconsider a = a, b = b as Element of L by A6, A7;
A11: 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
A12: a in C and
A13: not [a,("\/" X,L)] in R and
A14: not [("\/" X,L),a] in R ; :: thesis:
take a ; :: thesis:
thus a in C by A12; :: thesis:
a is_>=_than X

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

per cases in R or [x,a] in R or a = x ) by A12, A15, Def3;

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

( a <= a & x <= "\/" X,L ) by A1, A15, YELLOW_4:1;
hence x <= a by A13, A16, WAYBEL_4:def 5; :: thesis:

end;

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

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

end;

then "\/" X,L <= a by A1, YELLOW_0:def 9;
hence "\/" X,L < a by A3, A12, ORDERS_2:def 10; :: thesis:
thus not [("\/" X,L),a] in R by A14; :: thesis:

end;

per cases by A6, A7, 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 A8, A9, A10, 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 A8, A10, A11; :: 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 A8, A10, A11; :: 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 A9; :: thesis:

end;

then consider cs being Element of L such that
A17: cs in C and
A18: "\/" X,L < cs and
A19: not [("\/" X,L),cs] in R ;
take cs ; :: thesis:
thus ( cs in C & "\/" X,L < cs & not [("\/" X,L),cs] in R ) by A17, A18, A19; :: thesis:
A20: the carrier of (subrelstr C) = C by YELLOW_0:def 15;
reconsider cs1 = cs as Element of (subrelstr C) by A17, YELLOW_0:def 15;
take cs1 ; :: thesis:
thus cs = cs1 ; :: thesis:
A21: "\/" X,L <= cs by A18, ORDERS_2:def 10;
thus X is_<=_than cs1 :: thesis:

let b be Element of (subrelstr C); :: according to LATTICE3:def 9 :: thesis:
assume A22: b in X ; :: thesis:
reconsider b0 = b as Element of L by YELLOW_0:59;
b0 <= "\/" X,L by A1, A22, YELLOW_4:1;
then b0 <= cs by A21, ORDERS_2:26;
hence b <= cs1 by YELLOW_0:61; :: thesis:

end;

let a be Element of (subrelstr C); :: thesis:
reconsider a0 = a as Element of L by YELLOW_0:59;
assume X is_<=_than a ; :: thesis:
then X is_<=_than a0 by A20, YELLOW_0:63;
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 A20, Def3;
then cs <= a0 by A19, A23, A24, WAYBEL_4:def 4, WAYBEL_4:def 5;
hence cs1 <= a by YELLOW_0:61; :: thesis: