reconsider P = plane ((0* n),(1* n),(1* n)) as Subset of (REAL n) ;
P in plane_of_REAL n ;
hence not plane_of_REAL n is empty ; :: thesis: verum