let M be non empty Reflexive MetrStruct ; :: thesis: for K being SimplicialComplexStr st K is M bounded holds
0 <= diameter (M,K)
let K be SimplicialComplexStr; :: thesis: ( K is M bounded implies 0 <= diameter (M,K) )
assume A1: K is M bounded ; :: thesis: 0 <= diameter (M,K)

per cases ( the topology of K meets bool ([#] M) or the topology of K misses bool ([#] M) ) ;

suppose A2: the topology of K meets bool ([#] M) ; :: thesis: 0 <= diameter (M,K)

then consider S being object such that
A3: S in the topology of K and
A4: S in bool ([#] M) by XBOOLE_0:3;
reconsider S = S as Subset of M by A4;
ex r being Real st
for A being Subset of M st A in the topology of K holds
( A is bounded & diameter A <= r ) by A1;
then diameter S >= 0 by A3, TBSP_1:21;
hence 0 <= diameter (M,K) by A1, A2, A3, Def3; :: thesis: verum

end;

suppose the topology of K misses bool ([#] M) ; :: thesis: 0 <= diameter (M,K)

hence 0 <= diameter (M,K) by A1, Def3; :: thesis: verum

end;

end;