theorem Th8: :: FIN_TOPO:8

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