let n be Nat; :: thesis: for A, B being Subset of (TOP-REAL n) st ( A is bounded or B is bounded ) holds
A /\ B is bounded
let A, B be Subset of (TOP-REAL n); :: thesis: ( ( A is bounded or B is bounded ) implies A /\ B is bounded )
assume A1: ( A is bounded or B is bounded ) ; :: thesis: A /\ B is bounded
per cases ( A is bounded or B is bounded ) by A1;
suppose A is bounded ; :: thesis: A /\ B is bounded
hence A /\ B is bounded by RLTOPSP1:42, XBOOLE_1:17; :: thesis: verum
end;
suppose B is bounded ; :: thesis: A /\ B is bounded
hence A /\ B is bounded by RLTOPSP1:42, XBOOLE_1:17; :: thesis: verum
end;
end;