A ` is dense by Lm2, Th51, TOPMETR:17;
hence IRRAT is boundary Subset of R^1 by TOPS_1:def 4; :: thesis: verum