set V0 = the free finite-rank Z_Module;
reconsider nilfunc = [: the carrier of ((0). the free finite-rank Z_Module), the carrier of ((0). the free finite-rank Z_Module):] --> (0. F_Real) as Function of [: the carrier of ((0). the free finite-rank Z_Module), the carrier of ((0). the free finite-rank Z_Module):], the carrier of F_Real ;
set X0 = GenLat (((0). the free finite-rank Z_Module),nilfunc);
reconsider X0 = GenLat (((0). the free finite-rank Z_Module),nilfunc) as non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed free finite-rank LatticeStr over INT.Ring ;
take X0 ; :: thesis: X0 is Z_Lattice-like
thus X0 is Z_Lattice-like by ThTrivialLat1; :: thesis: verum