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)
proof
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;
( 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;
hence DualLat L is Submodule of DivisibleMod L by A1, VECTSP_4:def 2; :: thesis: verum