per cases ( v is torsion or not v is torsion ) ;

suppose v is torsion ; :: thesis: not Lin {v} is divisible

hence not Lin {v} is divisible by LmFGND2; :: thesis: verum

end;

suppose not v is torsion ; :: thesis: not Lin {v} is divisible

hence not Lin {v} is divisible by LmFGND1; :: thesis: verum

end;

end;