now :: thesis: for r1, r2 being Real st ( for A being Subset of M st A in the topology of K holds
diameter A <= r1 ) & ( for r being Real st ( for A being Subset of M st A in the topology of K holds
diameter A <= r ) holds
r >= r1 ) & ( for A being Subset of M st A in the topology of K holds
diameter A <= r2 ) & ( for r being Real st ( for A being Subset of M st A in the topology of K holds
diameter A <= r ) holds
r >= r2 ) holds
r1 = r2

let r1, r2 be Real; :: thesis: ( ( for A being Subset of M st A in the topology of K holds
diameter A <= r1 ) & ( for r being Real st ( for A being Subset of M st A in the topology of K holds
diameter A <= r ) holds
r >= r1 ) & ( for A being Subset of M st A in the topology of K holds
diameter A <= r2 ) & ( for r being Real st ( for A being Subset of M st A in the topology of K holds
diameter A <= r ) holds
r >= r2 ) implies r1 = r2 )
assume A9: ( ( for A being Subset of M st A in the topology of K holds
diameter A <= r1 ) & ( for r being Real st ( for A being Subset of M st A in the topology of K holds
diameter A <= r ) holds
r >= r1 ) & ( for A being Subset of M st A in the topology of K holds
diameter A <= r2 ) & ( for r being Real st ( for A being Subset of M st A in the topology of K holds
diameter A <= r ) holds
r >= r2 ) ) ; :: thesis: r1 = r2
( r1 <= r2 & r2 <= r1 ) by A9;
hence r1 = r2 by XXREAL_0:1; :: thesis: verum

end;

hence for b₁, b₂ being Real holds
( ( the topology of K meets bool ([#] M) & ( for A being Subset of M st A in the topology of K holds
diameter A <= b₁ ) & ( for r being Real st ( for A being Subset of M st A in the topology of K holds
diameter A <= r ) holds
r >= b₁ ) & ( for A being Subset of M st A in the topology of K holds
diameter A <= b₂ ) & ( for r being Real st ( for A being Subset of M st A in the topology of K holds
diameter A <= r ) holds
r >= b₂ ) implies b₁ = b₂ ) & ( not the topology of K meets bool ([#] M) & b₁ = 0 & b₂ = 0 implies b₁ = b₂ ) ) ; :: thesis: verum