theorem ZMtoZL3: :: ZMODLAT1:4

for V being free finite-rank 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 finite-rank