:: deftheorem defines open FIN_TOPO:def 14 :
for FT being non empty RelStr
for IT being Subset of FT holds
( IT is open iff IT = IT ^i );