let R be non empty Reflexive MetrStruct ; :: thesis: for S being Subset of R st S is bounded holds
0 <= diameter S
let S be Subset of R; :: thesis: ( S is bounded implies 0 <= diameter S )
assume A1: S is bounded ; :: thesis: 0 <= diameter S

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

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

hence 0 <= diameter S by Def8; :: thesis: verum

end;

suppose A2: S <> {} ; :: thesis: 0 <= diameter S

set x = the Element of S;
reconsider x = the Element of S as Element of R by A2, TARSKI:def 3;
dist (x,x) <= diameter S by A1, A2, Def8;
hence 0 <= diameter S by METRIC_1:1; :: thesis: verum

end;

end;