theorem :: ROUGHS_5:52

for R being non empty RelStr
for x, y being Subset of R holds ((Flip (f_0 R)) . x) /\ ((Flip (f_0 R)) . y) = (Flip (f_0 R)) . (x /\ y) by Propm;