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 b1, b2 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 <= b1 ) & ( for r being Real st ( for A being Subset of M st A in the topology of K holds
diameter A <= r ) holds
r >= b1 ) & ( for A being Subset of M st A in the topology of K holds
diameter A <= b2 ) & ( for r being Real st ( for A being Subset of M st A in the topology of K holds
diameter A <= r ) holds
r >= b2 ) implies b1 = b2 ) & ( not the topology of K meets bool ([#] M) & b1 = 0 & b2 = 0 implies b1 = b2 ) ) ; :: thesis: verum