theorem :: ROUGHS_5:49

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