:: deftheorem defines GenLat ZMODLAT1:def 4 :
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) = LatticeStr(# the carrier of V, the addF of V,(0. V), the lmult of V,sc #);