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 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 by FUNCOP_1:45;
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 ;
reconsider X0 = X0 as non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed free finite-rank Z_Lattice-like LatticeStr over INT.Ring by ThTrivialLat1;
take X0 ; :: thesis: X0 is strict
thus X0 is strict ; :: thesis: verum