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