theorem :: FIN_TOPO:24

for FT being non empty RelStr
for A being Subset of FT st A is closed holds
A ` is open