A1: L .: = LattStr(# the carrier of L,the L_meet of L,the L_join of L #) by LATTICE2:def 2;
LattRel (L .: ) = (LattRel L) ~ by LATTICE3:20;
then A2: LattRel ((L .: ) .: ) = ((LattRel L) ~ ) ~ by LATTICE3:20;
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₁ ) ) )
reconsider X' = X as Subset of L by A1;
set a' = "\/" X',L;
A3: ( X' is_less_than "\/" X',L & ( for r being Element of L st X' is_less_than r holds
"\/" X',L [= r ) ) by LATTICE3:def 21;
reconsider a = "\/" X',L as Element of (L .: ) by A1;
A4: 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' )
assume A5: q' in X ; :: thesis: a [= q'
reconsider q = q' as Element of L by A1;
q [= "\/" X',L by A3, 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;

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 )
assume A6: b is_less_than X ; :: thesis: b [= a
reconsider b' = b as Element of L by A1;
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' )
assume A7: q in X' ; :: thesis: q [= b'
reconsider q' = q as Element of (L .: ) by A1;
b [= q' by A6, A7, 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;

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