for A, B being set
for R being Subset of [:A,B:] holds union ((.: R) .: A) c= R .: (union A)