theorem FlipF0: :: ROUGHS_5:29

for R being non empty RelStr
for x being Subset of R holds (Flip (f_0 R)) . x = { w where w is Element of R : (tau R) . w c= x }