theorem Th7: :: FIN_TOPO:7

for FT being non empty RelStr
for x being Element of FT
for A being Subset of FT holds
( x in A ^i iff U_FT x c= A )