let V be non trivial finitely-generated Z_Module; :: thesis: not V is divisible
per cases ( V is torsion or not V is torsion ) ;
suppose V is torsion ; :: thesis: not V is divisible
hence not V is divisible by LmFGND4; :: thesis: verum
end;
suppose B2: not V is torsion ; :: thesis: not V is divisible
assume V is divisible ; :: thesis: contradiction
then VectQuot (V,(torsion_part V)) is divisible by LMLT2;
hence contradiction by B2, LmFGND3; :: thesis: verum
end;
end;