theorem :: FINTOPO2:12

for FT being non empty RelStr
for x being Element of FT
for A being Subset of FT holds
( P_A (x,A) = TRUE iff x in A ) by Def4;