:: deftheorem Def5 defines P_e FINTOPO2:def 5 :
for FT being non empty RelStr
for x, y being Element of FT holds
( ( x = y implies P_e (x,y) = TRUE ) & ( not x = y implies P_e (x,y) = FALSE ) );