theorem :: FINTOPO6:11

for FT being non empty RelStr
for P being Subset of FT holds
( P is closed iff P ` is open )