( the topology of K meets bool ([#] M) implies ex d being Real st
( ( for A being Subset of M st A in the topology of K holds
diameter A <= d ) & ( for r being Real st ( for A being Subset of M st A in the topology of K holds
diameter A <= r ) holds
r >= d ) ) )

defpred S₁[ Subset of M] means ( $1 in the topology of K & $1 is bounded );
deffunc H₁( Subset of M) -> object = diameter $1;
set X = { H₁(S) where S is Subset of M : S₁[S] } ;

let x be object ; :: thesis:
assume x in { H₁(S) where S is Subset of M : S₁[S] } ; :: thesis:
then ex S being Subset of M st
( x = H₁(S) & S₁[S] ) ;
hence x is real ; :: thesis:

end;

then reconsider X = { H₁(S) where S is Subset of M : S₁[S] } as real-membered set by MEMBERED:def 3;
assume the topology of K meets bool ([#] M) ; :: thesis:
then consider B being object such that
A2: B in the topology of K and
A3: B in bool ([#] M) by XBOOLE_0:3;
reconsider B = B as Subset of M by A3;
consider rr being Real such that
A4: for A being Subset of M st A in the topology of K holds
( A is bounded & H₁(A) <= rr ) by A1;

now :: thesis:

let x be ExtReal; :: thesis:
assume x in X ; :: thesis:
then consider s being Subset of M such that
A5: ( x = H₁(s) & S₁[s] ) ;
thus x <= rr by A4, A5; :: thesis:

end;

then rr is UpperBound of X by XXREAL_2:def 1;
then A6: X is bounded_above by XXREAL_2:def 10;
B is bounded by A2, A4;
then H₁(B) in X by A2;
then reconsider sX = sup X as Real by A6;
take sX ; :: thesis:

hereby :: thesis:

let A be Subset of M; :: thesis:
assume A in the topology of K ; :: thesis:
then S₁[A] by A4;
then H₁(A) in X ;
hence H₁(A) <= sX by XXREAL_2:4; :: thesis:

end;

let r be Real; :: thesis:
assume A7: for A being Subset of M st A in the topology of K holds
diameter A <= r ; :: thesis:

now :: thesis:

let x be ExtReal; :: thesis:
assume x in X ; :: thesis:
then consider A being Subset of M such that
A8: ( x = H₁(A) & S₁[A] ) ;
thus x <= r by A7, A8; :: thesis:

end;

then r is UpperBound of X by XXREAL_2:def 1;
hence r >= sX by XXREAL_2:def 3; :: thesis:

end;

hence ( ( the topology of K meets bool ([#] M) implies ex b₁ being Real st
( ( 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₁ ) ) ) & ( not the topology of K meets bool ([#] M) implies ex b₁ being Real st b₁ = 0 ) ) ; :: thesis: