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