let n be Nat; :: thesis: for A, B being Subset of (TOP-REAL n) st A is bounded & B is bounded holds
A \/ B is bounded
let A, B be Subset of (TOP-REAL n); :: thesis: ( A is bounded & B is bounded implies A \/ B is bounded )
assume A is bounded ; :: thesis: ( not B is bounded or A \/ B is bounded )
then A1: A is bounded Subset of (Euclid n) by JORDAN2C:11;
then reconsider A = A as Subset of (Euclid n) ;
assume B is bounded ; :: thesis: A \/ B is bounded
then A2: B is bounded Subset of (Euclid n) by JORDAN2C:11;
then reconsider B = B as Subset of (Euclid n) ;
reconsider E = A \/ B as Subset of (Euclid n) ;
E is bounded Subset of (Euclid n) by A1, A2, TBSP_1:13;
hence A \/ B is bounded by JORDAN2C:11; :: thesis: verum