for x1, y1, x2, y2 being set holds (x1 U+ y1) /\ (x2 U+ y2) = (x1 /\ x2) U+ (y1 /\ y2)