let L be positive-definite RATional Z_Lattice; :: thesis: DualLat L is Submodule of DivisibleMod L

A1: the carrier of (DualLat L) c= the carrier of (DivisibleMod L)

hence DualLat L is Submodule of DivisibleMod L by A1, VECTSP_4:def 2; :: thesis: verum

A1: the carrier of (DualLat L) c= the carrier of (DivisibleMod L)

proof

( 0. (DualLat L) = 0. (DivisibleMod L) & the addF of (DualLat L) = the addF of (DivisibleMod L) || the carrier of (DualLat L) & the lmult of (DualLat L) = the lmult of (DivisibleMod L) | [: the carrier of INT.Ring, the carrier of (DualLat L):] )
by defDualLat;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of (DualLat L) or x in the carrier of (DivisibleMod L) )

assume B1: x in the carrier of (DualLat L) ; :: thesis: x in the carrier of (DivisibleMod L)

x in DualSet L by B1, defDualLat;

then consider v being Dual of L such that

B2: x = v ;

thus x in the carrier of (DivisibleMod L) by B2; :: thesis: verum

end;assume B1: x in the carrier of (DualLat L) ; :: thesis: x in the carrier of (DivisibleMod L)

x in DualSet L by B1, defDualLat;

then consider v being Dual of L such that

B2: x = v ;

thus x in the carrier of (DivisibleMod L) by B2; :: thesis: verum

hence DualLat L is Submodule of DivisibleMod L by A1, VECTSP_4:def 2; :: thesis: verum