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 Th10;
hence proj2_3 X c= proj2_3 Y by Th11; :: thesis: verum