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