:: deftheorem Def2 defines P_2 FINTOPO2:def 2 :
for FT being non empty RelStr
for x, y being Element of FT
for A being Subset of FT holds
( ( y in U_FT x & y in A ` implies P_2 (x,y,A) = TRUE ) & ( ( not y in U_FT x or not y in A ` ) implies P_2 (x,y,A) = FALSE ) );