consider y being Point of Y;
take Sspace y ; :: thesis: ( Sspace y is trivial & Sspace y is strict & not Sspace y is empty )
thus ( Sspace y is trivial & Sspace y is strict & not Sspace y is empty ) by Lm2; :: thesis: verum