theorem :: ROUGHS_5:50

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