let Y be non empty TopStruct ; :: thesis: for y being Point of Y holds
( Sspace y is proper iff {y} is proper )
let y be Point of Y; :: thesis: ( Sspace y is proper iff {y} is proper )

hereby :: thesis: ( {y} is proper implies Sspace y is proper )

reconsider A = the carrier of (Sspace y) as Subset of Y by Lm1;
assume A1: Sspace y is proper ; :: thesis: {y} is proper
A = {y} by Def2;
hence {y} is proper by A1; :: thesis: verum

end;

thus ( {y} is proper implies Sspace y is proper ) by Def2; :: thesis: verum