theorem :: ROUGHS_5:44

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