let A be Subset of R^1 ; :: thesis: for a, b being real number st A = RAT a,b holds
Int A = {}
let a, b be real number ; :: thesis: ( A = RAT a,b implies Int A = {} )
assume A1: A = RAT a,b ; :: thesis: Int A = {}
A ` = REAL \ A by TOPMETR:24
.= (].-infty ,a.] \/ (IRRAT a,b)) \/ [.b,+infty .[ by A1, BORSUK_5:85 ;
then Cl (A ` ) = [#] R^1 by Th30;
then (Cl (A ` )) ` = {} R^1 by XBOOLE_1:37;
hence Int A = {} by TOPS_1:def 1; :: thesis: verum