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