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;

per cases ( V = {} or V <> {} ) ;

suppose V = {} ; :: thesis: diameter V <= diameter S

then diameter V = 0 by Def8;
hence diameter V <= diameter S by A1, Th21; :: thesis: verum

end;

suppose A4: V <> {} ; :: thesis: diameter V <= diameter S

for x, y being Point of R st x in V & y in V holds
dist (x,y) <= diameter S by A1, A2, Def8;
hence diameter V <= diameter S by A3, A4, Def8; :: thesis: verum

end;

end;