let n be Element of 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 A1: A is bounded Subset of (Euclid n) ; :: according to JORDAN2C:def 1 :: thesis: ( not B is Bounded or A \/ B is Bounded )
then reconsider A = A as Subset of (Euclid n) ;
assume A2: B is bounded Subset of (Euclid n) ; :: according to JORDAN2C:def 1 :: thesis: A \/ B is Bounded
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:def 1; :: thesis: verum