let V be free finite-rank Z_Module; :: thesis: 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
let sc be Function of [: the carrier of V, the carrier of V:], the carrier of F_Real; :: thesis: GenLat (V,sc) is finite-rank
set L = GenLat (V,sc);
GenLat (V,sc) is Submodule of V by LmZMtoZL1;
hence GenLat (V,sc) is finite-rank ; :: thesis: verum