consider x being Point of ;
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