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