theorem :: ROUGHS_5:53

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