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_inf_of (uparrow ("\/" X,L)) /\ C,L & ex_sup_of X,L & C is maximal holds
( "\/" X,(subrelstr C) = "/\" ((uparrow ("\/" X,L)) /\ C),L & ( not "\/" X,L in C implies "\/" X,L < "/\" ((uparrow ("\/" X,L)) /\ C),L ) )
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_inf_of (uparrow ("\/" X,L)) /\ C,L & ex_sup_of X,L & C is maximal holds
( "\/" X,(subrelstr C) = "/\" ((uparrow ("\/" X,L)) /\ C),L & ( not "\/" X,L in C implies "\/" X,L < "/\" ((uparrow ("\/" X,L)) /\ C),L ) )
let C be non empty strict_chain of R; :: thesis: for X being Subset of C st ex_inf_of (uparrow ("\/" X,L)) /\ C,L & ex_sup_of X,L & C is maximal holds
( "\/" X,(subrelstr C) = "/\" ((uparrow ("\/" X,L)) /\ C),L & ( not "\/" X,L in C implies "\/" X,L < "/\" ((uparrow ("\/" X,L)) /\ C),L ) )
let X be Subset of C; :: thesis: ( ex_inf_of (uparrow ("\/" X,L)) /\ C,L & ex_sup_of X,L & C is maximal implies ( "\/" X,(subrelstr C) = "/\" ((uparrow ("\/" X,L)) /\ C),L & ( not "\/" X,L in C implies "\/" X,L < "/\" ((uparrow ("\/" X,L)) /\ C),L ) ) )
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: ( "\/" X,(subrelstr C) = "/\" ((uparrow ("\/" X,L)) /\ C),L & ( not "\/" X,L in C implies "\/" X,L < "/\" ((uparrow ("\/" X,L)) /\ C),L ) )
A4: "\/" X,L <= "\/" X,L ;
reconsider x1 = "\/" X,(subrelstr C) as Element of L by YELLOW_0:59;
A5: the carrier of (subrelstr C) = C by YELLOW_0:def 15;

per cases ( "\/" X,L in C or not "\/" X,L in C ) ;

suppose A6: "\/" X,L in C ; :: thesis: ( "\/" X,(subrelstr C) = "/\" ((uparrow ("\/" X,L)) /\ C),L & ( not "\/" X,L in C implies "\/" X,L < "/\" ((uparrow ("\/" X,L)) /\ C),L ) )

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

proof

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

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: ( (uparrow ("\/" X,L)) /\ C is_>=_than a implies a <= x1 )
assume (uparrow ("\/" X,L)) /\ C is_>=_than a ; :: thesis: a <= x1
hence a <= x1 by A9, LATTICE3:def 8; :: thesis: verum

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: verum

end;

suppose not "\/" X,L in C ; :: thesis: ( "\/" X,(subrelstr C) = "/\" ((uparrow ("\/" X,L)) /\ C),L & ( not "\/" X,L in C implies "\/" X,L < "/\" ((uparrow ("\/" X,L)) /\ C),L ) )

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 10;
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: ( (uparrow ("\/" X,L)) /\ C is_>=_than a implies a <= cs )
assume (uparrow ("\/" X,L)) /\ C is_>=_than a ; :: thesis: a <= cs
hence a <= cs by A16, LATTICE3:def 8; :: thesis: verum

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: ( not b in (uparrow ("\/" X,L)) /\ C or cs <= b )
assume A19: b in (uparrow ("\/" X,L)) /\ C ; :: thesis: cs <= b
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 4, WAYBEL_4:def 5; :: thesis: verum

end;

ex_sup_of X, subrelstr C by A2, A3, Th11;
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: verum

end;

end;