theorem Th5: :: FIN_TOPO:5

for FT being non empty RelStr
for x being Element of FT
for A being Subset of FT holds
( x in A ^delta iff ( U_FT x meets A & U_FT x meets A ` ) )