let d be Real; :: thesis:
{} K is simplex-like ;
then {} M in the topology of K by PRE_TOPC:def 2;
then A1: the topology of K meets bool ([#] M) by XBOOLE_0:3;

hereby :: thesis:

assume A2: d = diameter (M,K) ; :: thesis:

hereby :: thesis:

let A be Subset of M; :: thesis:
assume A is Simplex of K ; :: thesis:
then A in the topology of K by PRE_TOPC:def 2;
hence diameter A <= d by A1, A2, Def3; :: thesis:

end;

let r be Real; :: thesis:
assume A3: for A being Subset of M st A is Simplex of K holds
diameter A <= r ; :: thesis:
for A being Subset of M st A in the topology of K holds
diameter A <= r by A3, PRE_TOPC:def 2;
hence r >= d by A1, A2, Def3; :: thesis:

end;

assume that
A4: for A being Subset of M st A is Simplex of K holds
diameter A <= d and
A5: for r being Real st ( for A being Subset of M st A is Simplex of K holds
diameter A <= r ) holds
r >= d ; :: thesis:
for A being Subset of M st A in the topology of K holds
diameter A <= d by A4, PRE_TOPC:def 2;
then A6: diameter (M,K) <= d by A1, Def3;

let A be Subset of M; :: thesis:
assume A is Simplex of K ; :: thesis:
then A in the topology of K by PRE_TOPC:def 2;
hence diameter A <= diameter (M,K) by A1, Def3; :: thesis:

end;

then d <= diameter (M,K) by A5;
hence d = diameter (M,K) by A6, XXREAL_0:1; :: thesis: