reconsider E = D as Subset of D byLm1; set G = { A where A is Subset of D : ( d0 in A & A <> D ) } ; set T = (bool D)\ { A where A is Subset of D : ( d0 in A & A <> D ) } ; set Y = TopStruct(# D,((bool D)\ { A where A is Subset of D : ( d0 in A & A <> D ) } ) #); thus STS (D,d0) is strict
; :: thesis: STS (D,d0) is TopSpace-like
for A being Subset of D holds ( not A = E or not d0 in A or not A <> D )
; then A1:
not E in { A where A is Subset of D : ( d0 in A & A <> D ) }
;