:: deftheorem Def4 defines P_A FINTOPO2:def 4 :
for FT being non empty RelStr
for x being Element of FT
for A being Subset of FT holds
( ( x in A implies P_A (x,A) = TRUE ) & ( not x in A implies P_A (x,A) = FALSE ) );