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 )

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

end;

hereby :: thesis: verum

assume {y} is proper ; :: thesis: Sspace y is proper
then for A being Subset of Y st A = the carrier of (Sspace y) holds
A is proper by Def4;
hence Sspace y is proper by Def3; :: thesis: verum

end;