for X, Y being set st X c= Y holds
proj1_3 X c= proj1_3 Y