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;