reconsider B = IRRAT as Subset of R^1 by TOPMETR:17;

let A be Subset of R^1; :: thesis: for a, b being Real st A = IRRAT (a,b) holds

Int A = {}

let a, b be Real; :: thesis: ( A = IRRAT (a,b) implies Int A = {} )

assume A = IRRAT (a,b) ; :: thesis: Int A = {}

then A = IRRAT /\ ].a,b.[ by BORSUK_5:def 3;

then A c= B by XBOOLE_1:17;

then A is boundary by TOPGEN_1:54, TOPS_3:11;

hence Int A = {} ; :: thesis: verum

let A be Subset of R^1; :: thesis: for a, b being Real st A = IRRAT (a,b) holds

Int A = {}

let a, b be Real; :: thesis: ( A = IRRAT (a,b) implies Int A = {} )

assume A = IRRAT (a,b) ; :: thesis: Int A = {}

then A = IRRAT /\ ].a,b.[ by BORSUK_5:def 3;

then A c= B by XBOOLE_1:17;

then A is boundary by TOPGEN_1:54, TOPS_3:11;

hence Int A = {} ; :: thesis: verum