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