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