let X, A, Y be set ; :: thesis: ( X c= A implies X \ Y c= A )
X \ Y c= X by Th36;
hence ( X c= A implies X \ Y c= A ) by Th1; :: thesis: verum