let V be non trivial free Z_Module; :: thesis: not V is divisible
set v = the non zero Vector of V;
not the non zero Vector of V is divisible by ThND1;
hence not V is divisible ; :: thesis: verum