theorem :: ZMODUL05:6
for V being free finite-rank Z_Module holds
( rank V = 2 iff ex u, v being VECTOR of V st
( u <> v & {u,v} is linearly-independent & (Omega). V = Lin {u,v} ) )