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