for R being non empty RelStr
for u, w being Element of R
for x being Subset of R st (tau R) . u = (tau R) . w holds
( u in (f_0 R) . x iff w in (f_0 R) . x )