:: deftheorem defines ^fi FIN_TOPO:def 18 :
for FT being non empty RelStr
for A being Subset of FT holds A ^fi = union { F where F is Subset of FT : ( A c= F & F is open ) } ;