theorem :: FINTOPO2:6

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