theorem :: XBOOLE_0:5

for X, Y being set
for x being object st X misses Y & x in X \/ Y & not ( x in X & not x in Y ) holds
( x in Y & not x in X ) by Def3, Th3;