theorem LmRank1: :: ZMODUL06:37
for V being torsion-free Z_Module
for v, u being Vector of V st v <> 0. V & u <> 0. V & (Lin {v}) /\ (Lin {u}) <> (0). V holds
rank ((Lin {v}) + (Lin {u})) = 1