let X be Subset of (L .:); :: according to VECTSP_8:def 6 :: thesis: ex b1 being Element of the carrier of (L .:) st
( b1 is_less_than X & ( for b2 being Element of the carrier of (L .:) holds
( not b2 is_less_than X or b2 [= b1 ) ) )
A1: L .: = LattStr(# the carrier of L, the L_meet of L, the L_join of L #) by LATTICE2:def 2;
then reconsider X9 = X as Subset of L ;
set a9 = "\/" (X9,L);
reconsider a = "\/" (X9,L) as Element of (L .:) by A1;
LattRel (L .:) = (LattRel L) ~ by LATTICE3:20;
then A2: LattRel ((L .:) .:) = ((LattRel L) ~) ~ by LATTICE3:20;
A3: for b being Element of (L .:) st b is_less_than X holds
b [= a
proof
let b be Element of (L .:); :: thesis: ( b is_less_than X implies b [= a )
reconsider b9 = b as Element of L by A1;
assume A4: b is_less_than X ; :: thesis: b [= a
X9 is_less_than b9
proof
let q be Element of L; :: according to LATTICE3:def 17 :: thesis: ( not q in X9 or q [= b9 )
reconsider q9 = q as Element of (L .:) by A1;
assume q in X9 ; :: thesis: q [= b9
then b [= q9 by A4;
then b % <= q9 % by LATTICE3:7;
then [(b %),(q9 %)] in the InternalRel of (LattPOSet (L .:)) by ORDERS_2:def 5;
then [(q9 %),(b %)] in the InternalRel of (LattPOSet (L .:)) ~ by RELAT_1:def 7;
then [(q9 %),(b %)] in the InternalRel of (LattPOSet ((L .:) .:)) by LATTICE3:20;
then q % <= b9 % by A2, ORDERS_2:def 5;
hence q [= b9 by LATTICE3:7; :: thesis: verum
end;
then "\/" (X9,L) [= b9 by LATTICE3:def 21;
then ("\/" (X9,L)) % <= b9 % by LATTICE3:7;
then [(("\/" (X9,L)) %),(b9 %)] in the InternalRel of (LattPOSet L) by ORDERS_2:def 5;
then [(b9 %),(("\/" (X9,L)) %)] in the InternalRel of (LattPOSet L) ~ by RELAT_1:def 7;
then [(b9 %),(("\/" (X9,L)) %)] in the InternalRel of (LattPOSet (L .:)) by LATTICE3:20;
then b % <= a % by ORDERS_2:def 5;
hence b [= a by LATTICE3:7; :: thesis: verum
end;
A5: X9 is_less_than "\/" (X9,L) by LATTICE3:def 21;
a is_less_than X
proof
let q9 be Element of (L .:); :: according to LATTICE3:def 16 :: thesis: ( not q9 in X or a [= q9 )
reconsider q = q9 as Element of L by A1;
assume q9 in X ; :: thesis: a [= q9
then q [= "\/" (X9,L) by A5;
then q % <= ("\/" (X9,L)) % by LATTICE3:7;
then [(q %),(("\/" (X9,L)) %)] in the InternalRel of (LattPOSet L) by ORDERS_2:def 5;
then [(("\/" (X9,L)) %),(q %)] in the InternalRel of (LattPOSet L) ~ by RELAT_1:def 7;
then [(("\/" (X9,L)) %),(q %)] in the InternalRel of (LattPOSet (L .:)) by LATTICE3:20;
then a % <= q9 % by ORDERS_2:def 5;
hence a [= q9 by LATTICE3:7; :: thesis: verum
end;
hence ex b1 being Element of the carrier of (L .:) st
( b1 is_less_than X & ( for b2 being Element of the carrier of (L .:) holds
( not b2 is_less_than X or b2 [= b1 ) ) ) by A3; :: thesis: verum