set m = the Element of M;
take K = Complex_of {({} X)}; :: thesis: ( K is M bounded & not K is void )
K is M bounded

proof

take r = diameter ({} M); :: according to SIMPLEX2:def 2 :: thesis: for A being Subset of M st A in the topology of K holds
( A is bounded & diameter A <= r )
let A be Subset of M; :: thesis: ( A in the topology of K implies ( A is bounded & diameter A <= r ) )
A1: the topology of K = bool ({} X) by SIMPLEX0:4;
assume A in the topology of K ; :: thesis: ( A is bounded & diameter A <= r )
hence ( A is bounded & diameter A <= r ) by A1; :: thesis: verum

end;

hence ( K is M bounded & not K is void ) ; :: thesis: verum