theorem Th22: :: TEX_1:22

for D being non empty set
for d0 being Element of D
for A being Subset of (STS (D,d0)) holds
( ( A c= D \ {d0} implies A is open ) & ( A <> D & A is open implies A c= D \ {d0} ) )