theorem Th2: :: GLIBPRE0:2

for X, Y, Z being set holds X /\ Z misses Y \ Z