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