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

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