theorem :: PRE_TOPC:12

for T being TopStruct
for A being Subset of T st A <> {} T holds
ex x being Point of T st x in A