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