theorem :: FINTOPO2:7

for FT being non empty RelStr
for x, y being Element of FT
for A being Subset of FT holds
( P_2 (x,y,A) = TRUE iff ( y in U_FT x & y in A ` ) ) by Def2;