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