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