theorem Th8: :: FINTOPO2:8

for FT being non empty RelStr
for x being Element of FT
for A being Subset of FT holds
( x in A ^delta iff ex y1, y2 being Element of FT st
( P_1 (x,y1,A) = TRUE & P_2 (x,y2,A) = TRUE ) )