theorem :: ROUGHS_5:47

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