|(p,(0. (TOP-REAL n)))| = 0 by EUCLID_2:32;
then |(p,(q - q))| = 0 by RLVECT_1:5;
then q in Plane (p,q) ;
hence (TOP-REAL n) | (Plane (p,q)) is non empty SubSpace of TOP-REAL n ; :: thesis: verum