let n be Element of NAT ; :: thesis: for A, B being Subset of (TOP-REAL n) st B is Bounded & A c= B holds
A is Bounded
let A, B be Subset of (TOP-REAL n); :: thesis: ( B is Bounded & A c= B implies A is Bounded )
assume A1: ( B is Bounded & A c= B ) ; :: thesis: A is Bounded
then reconsider C = B as bounded Subset of (Euclid n) by Def2;
A2: A c= C by A1;
reconsider C2 = A as Subset of (Euclid n) by TOPREAL3:13;
C2 is bounded by A2, TBSP_1:21;
hence A is Bounded by Def2; :: thesis: verum