let A be Subset of R^1 ; :: thesis: ( A = REAL implies not A is boundary )
assume A1: A = REAL ; :: thesis: not A is boundary
[#] R^1 = REAL by TOPMETR:24;
then Int A = A by A1, TOPS_1:43;
hence not A is boundary by A1; :: thesis: verum