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