A1: DualLat L is Submodule of DivisibleMod L by ThDL2;
the scalar of (DualLat L) = (ScProductDM L) || the carrier of (DualLat L) by defDualLat;
hence DualLat L is positive-definite by A1, ThSLGM3; :: thesis: verum