let X, Y be set ; :: thesis: ( X c= Y implies proj2_3 X c= proj2_3 Y )
assume X c= Y ; :: thesis: proj2_3 X c= proj2_3 Y
then proj1 X c= proj1 Y by Th8;
hence proj2_3 X c= proj2_3 Y by Th9; :: thesis: verum