let A be Subset of R^1 ; :: thesis: ( REAL = A ` implies A = {} )
reconsider AB = {} R^1 as Subset of R^1 ;
assume REAL = A ` ; :: thesis: A = {}
then AB ` = A ` by TOPMETR:24;
then AB = (A ` ) ` ;
hence A = {} ; :: thesis: verum