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,()) = "/\" (((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,()) = "/\" (((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,()) = "/\" (((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,()) = "/\" (((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,());
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,()) = "/\" (((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,()) as Element of L by YELLOW_0:58;
A5: the carrier of () = 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,()) = "/\" (((uparrow ("\/" (X,L))) /\ C),L) & ( not "\/" (X,L) in C implies "\/" (X,L) < "/\" (((uparrow ("\/" (X,L))) /\ C),L) ) )
then A7: "\/" (X,L) = "\/" (X,()) by ;
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 ; :: 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 ;
then A9: x1 in (uparrow ("\/" (X,L))) /\ C by ;
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; :: thesis: verum
end;
hence ( "\/" (X,()) = "/\" (((uparrow ("\/" (X,L))) /\ C),L) & ( not "\/" (X,L) in C implies "\/" (X,L) < "/\" (((uparrow ("\/" (X,L))) /\ C),L) ) ) by ; :: thesis: verum
end;
suppose not "\/" (X,L) in C ; :: thesis: ( "\/" (X,()) = "/\" (((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 () st
( cs = cs1 & X is_<=_than cs1 & ( for a being Element of () st X is_<=_than a holds
cs1 <= a ) ) by A2, A3, Lm2;
A14: "\/" (X,L) <= cs by ;
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 ;
then A16: cs in (uparrow ("\/" (X,L))) /\ C by ;
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; :: 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 ;
then ( [b,cs] in R or b = cs or [cs,b] in R ) by ;
hence cs <= b by ; :: thesis: verum
end;
ex_sup_of X, subrelstr C by A2, A3, Th8;
then cs = "\/" (X,()) by ;
hence ( "\/" (X,()) = "/\" (((uparrow ("\/" (X,L))) /\ C),L) & ( not "\/" (X,L) in C implies "\/" (X,L) < "/\" (((uparrow ("\/" (X,L))) /\ C),L) ) ) by ; :: thesis: verum
end;
end;