set y = the Point of Y;
take Sspace the Point of Y ; :: thesis: ( Sspace the Point of Y is strict & Sspace the Point of Y is 1 -element )
thus ( Sspace the Point of Y is strict & Sspace the Point of Y is 1 -element ) by Lm2; :: thesis: verum