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