let A be Subset of R^1 ; :: thesis: for a, b being real number st A = IRRAT a,b holds
Int A = {}
let a, b be real number ; :: thesis: ( A = IRRAT a,b implies Int A = {} )
assume A1: A = IRRAT a,b ; :: thesis: Int A = {}
reconsider B = IRRAT as Subset of R^1 by TOPMETR:24;
A = IRRAT /\ ].a,b.[ by A1, BORSUK_5:def 5;
then A c= B by XBOOLE_1:17;
then A is boundary by TOPGEN_1:57, TOPS_3:11;
hence Int A = {} ; :: thesis: verum