theorem :: FINTOPO2:16

for FT being non empty RelStr
for x being Element of FT
for A being Subset of FT holds
( x in A ^s iff ( P_A (x,A) = TRUE & ( for y being Element of FT holds
( not P_1 (x,y,A) = TRUE or not P_e (x,y) = FALSE ) ) ) )