let X, Y, Z be set ; :: thesis: ( X c= Y & Y misses Z implies X misses Z )
assume ( X c= Y & Y /\ Z = {} ) ; :: according to XBOOLE_0:def 7 :: thesis: X misses Z
then X /\ Z = {} by Th3, Th26;
hence X misses Z by XBOOLE_0:def 7; :: thesis: verum