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;