set A = DualSet L;
reconsider A = DualSet L as non empty Subset of (DivisibleMod L) ;
set ad = the addF of (DivisibleMod L) || A;
dom the addF of (DivisibleMod L) = [: the carrier of (DivisibleMod L), the carrier of (DivisibleMod L):] by FUNCT_2:def 1;
then A3: dom ( the addF of (DivisibleMod L) || A) = [: the carrier of (DivisibleMod L), the carrier of (DivisibleMod L):] /\ [:A,A:] by RELAT_1:61
.= [:A,A:] by XBOOLE_1:28 ;
for x being object st x in [:A,A:] holds
( the addF of (DivisibleMod L) || A) . x in A

let x be object ; :: thesis:
assume B1: x in [:A,A:] ; :: thesis:
then consider x1, x2 being object such that
B2: ( x1 in A & x2 in A & x = [x1,x2] ) by ZFMISC_1:def 2;
reconsider v1 = x1, v2 = x2 as Vector of (DivisibleMod L) by B2;
( the addF of (DivisibleMod L) || A) . (x1,x2) = v1 + v2 by B1, B2, FUNCT_1:49;
hence ( the addF of (DivisibleMod L) || A) . x in A by B2, VECTSP_4:def 1; :: thesis:

end;

then reconsider ad = the addF of (DivisibleMod L) || A as Function of [:A,A:],A by A3, FUNCT_2:3;
A6: [: the carrier of INT.Ring,A:] c= [: the carrier of INT.Ring, the carrier of (DivisibleMod L):] by ZFMISC_1:95;
set mu = the lmult of (DivisibleMod L) | [: the carrier of INT.Ring,A:];
dom the lmult of (DivisibleMod L) = [: the carrier of INT.Ring, the carrier of (DivisibleMod L):] by FUNCT_2:def 1;
then A4: dom ( the lmult of (DivisibleMod L) | [: the carrier of INT.Ring,A:]) = [: the carrier of INT.Ring, the carrier of (DivisibleMod L):] /\ [: the carrier of INT.Ring,A:] by RELAT_1:61
.= [: the carrier of INT.Ring,A:] by A6, XBOOLE_1:28 ;
for x being object st x in [: the carrier of INT.Ring,A:] holds
( the lmult of (DivisibleMod L) | [: the carrier of INT.Ring,A:]) . x in A

let x be object ; :: thesis:
assume B1: x in [: the carrier of INT.Ring,A:] ; :: thesis:
then consider x1, x2 being object such that
B2: ( x1 in INT & x2 in A & x = [x1,x2] ) by ZFMISC_1:def 2;
reconsider i1 = x1 as Element of INT.Ring by B2;
reconsider v2 = x2 as Vector of (DivisibleMod L) by B2;
( the lmult of (DivisibleMod L) | [: the carrier of INT.Ring,A:]) . (x1,x2) = i1 * v2 by B1, B2, FUNCT_1:49;
hence ( the lmult of (DivisibleMod L) | [: the carrier of INT.Ring,A:]) . x in A by B2, VECTSP_4:def 1; :: thesis:

end;

then reconsider mu = the lmult of (DivisibleMod L) | [: the carrier of INT.Ring,A:] as Function of [: the carrier of INT.Ring,A:],A by A4, FUNCT_2:3;
set sc = (ScProductDM L) || A;
dom (ScProductDM L) = [: the carrier of (DivisibleMod L), the carrier of (DivisibleMod L):] by FUNCT_2:def 1;
then A5: dom ((ScProductDM L) || A) = [: the carrier of (DivisibleMod L), the carrier of (DivisibleMod L):] /\ [:A,A:] by RELAT_1:61
.= [:A,A:] by XBOOLE_1:28 ;
for x being object st x in [:A,A:] holds
((ScProductDM L) || A) . x in the carrier of F_Real

let x be object ; :: thesis:
assume B1: x in [:A,A:] ; :: thesis:
then consider x1, x2 being object such that
B2: ( x1 in A & x2 in A & x = [x1,x2] ) by ZFMISC_1:def 2;
reconsider v1 = x1, v2 = x2 as Vector of (DivisibleMod L) by B2;
((ScProductDM L) || A) . (x1,x2) = (ScProductDM L) . (v1,v2) by B1, B2, FUNCT_1:49;
hence ((ScProductDM L) || A) . x in the carrier of F_Real by B2; :: thesis:

end;

then reconsider sc = (ScProductDM L) || A as Function of [:A,A:], the carrier of F_Real by A5, FUNCT_2:3;
reconsider ze = 0. (DivisibleMod L) as Element of A by ZMODUL01:18;
set L1 = LatticeStr(# A,ad,ze,mu,sc #);
reconsider L1 = LatticeStr(# A,ad,ze,mu,sc #) as non empty LatticeStr over INT.Ring ;
A7: L1 is Submodule of DivisibleMod L by ZMODLAT2:10;
reconsider L1 = L1 as non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed LatticeStr over INT.Ring by ZMODLAT2:10;
set I = the Basis of (EMLat L);
for v being Vector of (DivisibleMod L) st v in L1 holds
v in Lin (DualBasis the Basis of (EMLat L))

let v be Vector of (DivisibleMod L); :: thesis:
assume B1: v in L1 ; :: thesis:
consider x being Dual of L such that
B2: x = v by B1;
thus v in Lin (DualBasis the Basis of (EMLat L)) by B2, ThDE3; :: thesis:

end;

then L1 is Submodule of Lin (DualBasis the Basis of (EMLat L)) by A7, ZMODUL01:44;
then reconsider L1 = L1 as strict Z_Lattice by A7, ZMODLAT2:27;
take L1 ; :: thesis:
thus ( the carrier of L1 = DualSet L & 0. L1 = 0. (DivisibleMod L) & the addF of L1 = the addF of (DivisibleMod L) || the carrier of L1 & the lmult of L1 = the lmult of (DivisibleMod L) | [: the carrier of INT.Ring, the carrier of L1:] & the scalar of L1 = (ScProductDM L) || the carrier of L1 ) ; :: thesis: