:: deftheorem defines closed FIN_TOPO:def 15 :
for FT being non empty RelStr
for IT being Subset of FT holds
( IT is closed iff IT = IT ^b );