let N be non empty MetrStruct ; :: thesis: for C, D being Subset of N st C is bounded & D c= C holds
D is bounded
let C, D be Subset of N; :: thesis: ( C is bounded & D c= C implies D is bounded )
assume that
A1: C is bounded and
A2: D c= C ; :: thesis: D is bounded
consider r being Real such that
A3: 0 < r and
A4: for x, y being Point of N st x in C & y in C holds
dist (x,y) <= r by A1;
ex r being Real st
( 0 < r & ( for x, y being Point of N st x in D & y in D holds
dist (x,y) <= r ) )

proof

take r ; :: thesis: ( 0 < r & ( for x, y being Point of N st x in D & y in D holds
dist (x,y) <= r ) )
thus 0 < r by A3; :: thesis: for x, y being Point of N st x in D & y in D holds
dist (x,y) <= r
let x, y be Point of N; :: thesis: ( x in D & y in D implies dist (x,y) <= r )
assume ( x in D & y in D ) ; :: thesis: dist (x,y) <= r
hence dist (x,y) <= r by A2, A4; :: thesis: verum

end;

hence D is bounded ; :: thesis: verum