let n be 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) \/ (A /\ B) = A \ (B \ B) by XBOOLE_1:52
.= A \ {} by XBOOLE_1:37
.= A ;
A /\ B is bounded by A2, Th82;
hence not A \ B is bounded by A1, A3, Th65; :: thesis: verum