let X, Y, Z be set ; :: thesis: ( X c= Y implies X c= Z \/ Y )
Y c= Z \/ Y by Th7;
hence ( X c= Y implies X c= Z \/ Y ) by Th1; :: thesis: verum