:: deftheorem Def3 defines P_0 FINTOPO2:def 3 :
for FT being non empty RelStr
for x, y being Element of FT holds
( ( y in U_FT x implies P_0 (x,y) = TRUE ) & ( not y in U_FT x implies P_0 (x,y) = FALSE ) );