for a being Vector of V holds a + W in V .. W by Def12;
hence not V .. W is empty ; :: thesis: verum