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