reconsider L = Line (0* n),(1* n) as Subset of (REAL n) ;
L in line_of_REAL n ;
hence not line_of_REAL n is empty ; :: thesis: verum