let X, Y be set ; :: thesis: ( X c= Y implies proj2_4 X c= proj2_4 Y )
assume X c= Y ; :: thesis: proj2_4 X c= proj2_4 Y
then proj1_3 X c= proj1_3 Y by Th10;
hence proj2_4 X c= proj2_4 Y by Th9; :: thesis: verum