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;