theorem :: ROUGHS_5:46

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