let n be Element of NAT ; :: thesis: for A, B being Subset of (TOP-REAL n) st not A is Bounded & B is Bounded holds
not A \ B is Bounded
let A, B be Subset of (TOP-REAL n); :: thesis: ( not A is Bounded & B is Bounded implies not A \ B is Bounded )
assume that
A1: not A is Bounded and
A2: B is Bounded ; :: thesis: not A \ B is Bounded
A3: A /\ B is Bounded by A2, Th98;
(A \ B) \/ (A /\ B) = A \ (B \ B) by XBOOLE_1:52
.= A \ {} by XBOOLE_1:37
.= A ;
hence not A \ B is Bounded by A1, A3, Th76; :: thesis: verum