reconsider W = (0). V as strict free Submodule of V ;

take W ; :: thesis: ( W is strict & W is finite-rank )

thus ( W is strict & W is finite-rank ) ; :: thesis: verum

take W ; :: thesis: ( W is strict & W is finite-rank )

thus ( W is strict & W is finite-rank ) ; :: thesis: verum