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