:: deftheorem Def1 defines P_1 FINTOPO2:def 1 :
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_1 (x,y,A) = TRUE ) & ( ( not y in U_FT x or not y in A ) implies P_1 (x,y,A) = FALSE ) );