for FT being non empty RelStr
for A being Subset of FT holds
( A is open iff ( ( for z being Element of FT st U_FT z c= A holds
z in A ) & ( for x being Element of FT st x in A holds
U_FT x c= A ) ) )