let n be Element of 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 JORDAN2C:16, XBOOLE_1:17; :: thesis: verum

end;

suppose B is Bounded ; :: thesis: A /\ B is Bounded

hence A /\ B is Bounded by JORDAN2C:16, XBOOLE_1:17; :: thesis: verum

end;

end;