let Y be non empty TopStruct ; :: thesis: for y being Point of holds
( Sspace y is proper iff {y} is proper )
let y be Point of ; :: 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 by Lm1;
assume A1: Sspace y is proper ; :: thesis: {y} is proper
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 st A = the carrier of (Sspace y) holds
A is proper by Def4;
hence Sspace y is proper by Def3; :: thesis: verum

end;