let A, X, 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 ) ; :: thesis: verum