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:58;

A5: the carrier of (subrelstr C) = C by YELLOW_0:def 15;

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:58;

A5: the carrier of (subrelstr C) = C by YELLOW_0:def 15;

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

end;

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:64;

A8: (uparrow ("\/" (X,L))) /\ C is_>=_than x1

a <= x1

end;A8: (uparrow ("\/" (X,L))) /\ C is_>=_than x1

proof

for a being Element of L st (uparrow ("\/" (X,L))) /\ C is_>=_than a holds
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;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

a <= x1

proof

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
"\/" (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; :: thesis: verum

end;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; :: thesis: verum

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 6;

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

a <= cs

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

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;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

A17:
cs <= cs
;
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; :: thesis: verum

end;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; :: thesis: verum

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

proof

ex_sup_of X, subrelstr C
by A2, A3, Th8;
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 3, WAYBEL_4:def 4; :: thesis: verum

end;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 3, WAYBEL_4:def 4; :: thesis: verum

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