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 A1: ( C is bounded & D c= C ) ; :: thesis: D is bounded
then consider r being Real such that
A2: ( 0 < r & ( for x, y being Point of N st x in C & y in C holds
dist x,y <= r ) ) by Def9;
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 A2; :: 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 A1, A2; :: thesis: verum

end;

hence D is bounded by Def9; :: thesis: verum