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