theorem LmZMtoZL1: :: ZMODLAT1:2

for V being Z_Module
for sc being Function of [: the carrier of V, the carrier of V:], the carrier of F_Real holds GenLat (V,sc) is Submodule of V