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 X' = X as Subset of L ;
set a' = "\/" X',L;
reconsider a = "\/" X',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 b' = b as Element of L by A1;
assume A4: b is_less_than X ; :: thesis: b [= a
X' is_less_than b'

proof

let q be Element of L; :: according to LATTICE3:def 17 :: thesis: ( not q in X' or q [= b' )
reconsider q' = q as Element of (L .: ) by A1;
assume q in X' ; :: thesis: q [= b'
then b [= q' by A4, LATTICE3:def 16;
then b % <= q' % by LATTICE3:7;
then [(b % ),(q' % )] in the InternalRel of (LattPOSet (L .: )) by ORDERS_2:def 9;
then [(q' % ),(b % )] in the InternalRel of (LattPOSet (L .: )) ~ by RELAT_1:def 7;
then [(q' % ),(b % )] in the InternalRel of (LattPOSet ((L .: ) .: )) by LATTICE3:20;
then q % <= b' % by A2, ORDERS_2:def 9;
hence q [= b' by LATTICE3:7; :: thesis: verum

end;

then "\/" X',L [= b' by LATTICE3:def 21;
then ("\/" X',L) % <= b' % by LATTICE3:7;
then [(("\/" X',L) % ),(b' % )] in the InternalRel of (LattPOSet L) by ORDERS_2:def 9;
then [(b' % ),(("\/" X',L) % )] in the InternalRel of (LattPOSet L) ~ by RELAT_1:def 7;
then [(b' % ),(("\/" X',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: X' is_less_than "\/" X',L by LATTICE3:def 21;
a is_less_than X

proof

let q' be Element of (L .: ); :: according to LATTICE3:def 16 :: thesis: ( not q' in X or a [= q' )
reconsider q = q' as Element of L by A1;
assume q' in X ; :: thesis: a [= q'
then q [= "\/" X',L by A5, LATTICE3:def 17;
then q % <= ("\/" X',L) % by LATTICE3:7;
then [(q % ),(("\/" X',L) % )] in the InternalRel of (LattPOSet L) by ORDERS_2:def 9;
then [(("\/" X',L) % ),(q % )] in the InternalRel of (LattPOSet L) ~ by RELAT_1:def 7;
then [(("\/" X',L) % ),(q % )] in the InternalRel of (LattPOSet (L .: )) by LATTICE3:20;
then a % <= q' % by ORDERS_2:def 9;
hence a [= q' 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