reconsider B = IRRAT as Subset of R^1 by TOPMETR:17;
reconsider A = RAT as Subset of R^1 by NUMBERS:12, TOPMETR:17;
take A ; :: thesis: ex B being Subset of R^1 st
( A is boundary & B is boundary & not A \/ B is boundary )
take B ; :: thesis: ( A is boundary & B is boundary & not A \/ B is boundary )
A \/ B = RAT \/ REAL by BORSUK_5:def 1, XBOOLE_1:39
.= REAL by NUMBERS:12, XBOOLE_1:12 ;
hence ( A is boundary & B is boundary & not A \/ B is boundary ) by Th53, Th54, Th55; :: thesis: verum