for X, Y being set holds proj1_4 (X /\ Y) c= (proj1_4 X) /\ (proj1_4 Y)