let A be Subset of R^1 ; :: thesis: ( A = IRRAT implies A is boundary )
assume A = IRRAT ; :: thesis: A is boundary
then A ` is dense by Lm3, Th54, TOPMETR:24;
hence A is boundary by TOPS_1:def 4; :: thesis: verum