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: the carrier of (subrelstr C) = C by YELLOW_0:def 15;
A5: "\/" X,L <= "\/" X,L ;
reconsider x1 = "\/" X,(subrelstr C) as Element of L by YELLOW_0:59;

per cases ;

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

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

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;

let a be Element of L; :: thesis:
assume A9: (uparrow ("\/" X,L)) /\ C is_>=_than a ; :: thesis:
"\/" X,L in uparrow ("\/" X,L) by A5, WAYBEL_0:18;
then x1 in (uparrow ("\/" X,L)) /\ C by A6, A7, XBOOLE_0:def 4;
hence a <= x1 by A9, LATTICE3:def 8; :: 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, Lm3;
A14: cs <= cs ;
A15: "\/" X,L <= cs by A11, ORDERS_2:def 10;
ex_sup_of X, subrelstr C by A2, A3, Th11;
then A16: cs = "\/" X,(subrelstr C) by A13, YELLOW_0:def 9;
A17: (uparrow ("\/" X,L)) /\ C is_>=_than cs

let b be Element of L; :: according to LATTICE3:def 8 :: thesis:
assume A18: b in (uparrow ("\/" X,L)) /\ C ; :: thesis:
then b in uparrow ("\/" X,L) by XBOOLE_0:def 4;
then A19: "\/" X,L <= b by WAYBEL_0:18;
b in C by A18, 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, A14, A19, WAYBEL_4:def 4, WAYBEL_4:def 5; :: thesis:

end;

let a be Element of L; :: thesis:
assume A20: (uparrow ("\/" X,L)) /\ C is_>=_than a ; :: thesis:
cs in uparrow ("\/" X,L) by A15, WAYBEL_0:18;
then cs in (uparrow ("\/" X,L)) /\ C by A10, XBOOLE_0:def 4;
hence a <= cs by A20, LATTICE3:def 8; :: 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, A11, A16, A17, YELLOW_0:def 10; :: thesis:

end;