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 ) )

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

hence
D is bounded
; :: thesis: verum
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;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