let Y be non empty TopStruct ; :: thesis: for y being Point of Y st Sspace y is proper holds
not Y is trivial
let y be Point of Y; :: thesis: ( Sspace y is proper implies not Y is trivial )
assume Sspace y is proper ; :: thesis: not Y is trivial
then not Y is 1 -element ;
then not the carrier of Y is 1 -element by STRUCT_0:def 19;
hence not Y is trivial ; :: thesis: verum