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:
set s = "\/" (X,L);
set x = "\/" (X,(subrelstr C));
set U = uparrow ("\/" (X,L));
assume that
A1: ex_inf_of (uparrow ("\/" (X,L))) /\ C,L and
A2: ex_sup_of X,L and
A3: C is maximal ; :: thesis:
A4: "\/" (X,L) <= "\/" (X,L) ;
reconsider x1 = "\/" (X,(subrelstr C)) as Element of L by YELLOW_0:58;
A5: the carrier of (subrelstr C) = C by YELLOW_0:def 15;

per cases ;

suppose A6: "\/" (X,L) in C ; :: thesis:

then A7: "\/" (X,L) = "\/" (X,(subrelstr C)) by A2, A5, YELLOW_0:64;
A8: (uparrow ("\/" (X,L))) /\ C is_>=_than x1

proof

let b be Element of L; :: according to LATTICE3:def 8 :: thesis:
assume b in (uparrow ("\/" (X,L))) /\ C ; :: thesis:
then b in uparrow ("\/" (X,L)) by XBOOLE_0:def 4;
hence x1 <= b by A7, WAYBEL_0:18; :: thesis:

end;

for a being Element of L st (uparrow ("\/" (X,L))) /\ C is_>=_than a holds
a <= x1

proof

"\/" (X,L) in uparrow ("\/" (X,L)) by A4, WAYBEL_0:18;
then A9: x1 in (uparrow ("\/" (X,L))) /\ C by A6, A7, XBOOLE_0:def 4;
let a be Element of L; :: thesis:
assume (uparrow ("\/" (X,L))) /\ C is_>=_than a ; :: thesis:
hence a <= x1 by A9; :: thesis:

end;

hence ( "\/" (X,(subrelstr C)) = "/\" (((uparrow ("\/" (X,L))) /\ C),L) & ( not "\/" (X,L) in C implies "\/" (X,L) < "/\" (((uparrow ("\/" (X,L))) /\ C),L) ) ) by A1, A6, A8, YELLOW_0:def 10; :: thesis:

end;

suppose not "\/" (X,L) in C ; :: thesis:

then consider cs being Element of L such that
A10: cs in C and
A11: "\/" (X,L) < cs and
A12: not [("\/" (X,L)),cs] in R and
A13: 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 ) ) by A2, A3, Lm2;
A14: "\/" (X,L) <= cs by A11, ORDERS_2:def 6;
A15: for a being Element of L st (uparrow ("\/" (X,L))) /\ C is_>=_than a holds
a <= cs

proof

cs in uparrow ("\/" (X,L)) by A14, WAYBEL_0:18;
then A16: cs in (uparrow ("\/" (X,L))) /\ C by A10, XBOOLE_0:def 4;
let a be Element of L; :: thesis:
assume (uparrow ("\/" (X,L))) /\ C is_>=_than a ; :: thesis:
hence a <= cs by A16; :: thesis:

end;

A17: cs <= cs ;
A18: (uparrow ("\/" (X,L))) /\ C is_>=_than cs

proof

let b be Element of L; :: according to LATTICE3:def 8 :: thesis:
assume A19: b in (uparrow ("\/" (X,L))) /\ C ; :: thesis:
then b in uparrow ("\/" (X,L)) by XBOOLE_0:def 4;
then A20: "\/" (X,L) <= b by WAYBEL_0:18;
b in C by A19, XBOOLE_0:def 4;
then ( [b,cs] in R or b = cs or [cs,b] in R ) by A10, Def3;
hence cs <= b by A12, A17, A20, WAYBEL_4:def 3, WAYBEL_4:def 4; :: thesis:

end;

ex_sup_of X, subrelstr C by A2, A3, Th8;
then cs = "\/" (X,(subrelstr C)) by A13, YELLOW_0:def 9;
hence ( "\/" (X,(subrelstr C)) = "/\" (((uparrow ("\/" (X,L))) /\ C),L) & ( not "\/" (X,L) in C implies "\/" (X,L) < "/\" (((uparrow ("\/" (X,L))) /\ C),L) ) ) by A15, A1, A11, A18, YELLOW_0:def 10; :: thesis:

end;

end;