let A, B, X, Y be set ; :: thesis: ( A c= X & B c= Y & X misses Y implies A misses B )
assume that
A1: A c= X and
A2: B c= Y and
A3: X misses Y ; :: thesis: A misses B
A misses Y by A1, A3, Th63;
hence A misses B by A2, Th63; :: thesis: verum