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 that
A1: B is Bounded and
A2: A c= B ; :: thesis: A is Bounded
reconsider C2 = A as Subset of (Euclid n) by TOPREAL3:8;
reconsider C = B as bounded Subset of (Euclid n) by A1, Def2;
A c= C by A2;
then C2 is bounded by TBSP_1:14;
hence A is Bounded by Def2; :: thesis: verum