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 ) ; :: thesis: verum