theorem :: ROUGHS_5:43

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