consider x being Point of X;
take Sspace x ; :: thesis: ( Sspace x is trivial & Sspace x is strict & Sspace x is TopSpace-like & not Sspace x is empty )
thus ( Sspace x is trivial & Sspace x is strict & Sspace x is TopSpace-like & not Sspace x is empty ) ; :: thesis: verum