let X be set ; :: thesis: for M being non empty Reflexive MetrStruct
for K being b₁ bounded SimplicialComplexStr of X
for KX being SubSimplicialComplex of K holds diameter (M,KX) <= diameter (M,K)
let M be non empty Reflexive MetrStruct ; :: thesis: for K being M bounded SimplicialComplexStr of X
for KX being SubSimplicialComplex of K holds diameter (M,KX) <= diameter (M,K)
let K be M bounded SimplicialComplexStr of X; :: thesis: for KX being SubSimplicialComplex of K holds diameter (M,KX) <= diameter (M,K)
let KX be SubSimplicialComplex of K; :: thesis: diameter (M,KX) <= diameter (M,K)
A1: the topology of KX c= the topology of K by SIMPLEX0:def 13;

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

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

then the topology of K meets bool ([#] M) by A1, XBOOLE_1:63;
then for A being Subset of M st A in the topology of KX holds
diameter A <= diameter (M,K) by A1, Def3;
hence diameter (M,KX) <= diameter (M,K) by A2, Def3; :: thesis: verum

end;

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

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

end;

end;