let X be Subset of (L .: ); :: according to VECTSP_8:def 6 :: thesis: ex b₁ being Element of the carrier of (L .: ) st
( b₁ is_less_than X & ( for b₂ being Element of the carrier of (L .: ) holds
( not b₂ is_less_than X or b₂ [= b₁ ) ) )
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, LATTICE3:def 16;
then b % <= q9 % by LATTICE3:7;
then [(b % ),(q9 % )] in the InternalRel of (LattPOSet (L .: )) by ORDERS_2:def 9;
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 9;
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 9;
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 9;
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, LATTICE3:def 17;
then q % <= ("\/" X9,L) % by LATTICE3:7;
then [(q % ),(("\/" X9,L) % )] in the InternalRel of (LattPOSet L) by ORDERS_2:def 9;
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 9;
hence a [= q9 by LATTICE3:7; :: thesis: verum

end;

hence ex b₁ being Element of the carrier of (L .: ) st
( b₁ is_less_than X & ( for b₂ being Element of the carrier of (L .: ) holds
( not b₂ is_less_than X or b₂ [= b₁ ) ) ) by A3; :: thesis: verum