let R be non empty Reflexive MetrStruct ; :: thesis: for S, V being Subset of R st S is bounded & V c= S holds

diameter V <= diameter S

let S, V be Subset of R; :: thesis: ( S is bounded & V c= S implies diameter V <= diameter S )

assume that

A1: S is bounded and

A2: V c= S ; :: thesis: diameter V <= diameter S

A3: V is bounded by A1, A2, Th14;

diameter V <= diameter S

let S, V be Subset of R; :: thesis: ( S is bounded & V c= S implies diameter V <= diameter S )

assume that

A1: S is bounded and

A2: V c= S ; :: thesis: diameter V <= diameter S

A3: V is bounded by A1, A2, Th14;