let V be RealUnitarySpace; :: thesis: for W1, W2 being Subspace of V holds 0. W1 = 0. W2
let W1, W2 be Subspace of V; :: thesis: 0. W1 = 0. W2
0. W1 = 0. V by Def1;
hence 0. W1 = 0. W2 by Def1; :: thesis: verum