theorem :: INTERVA1:4

for U being set
for A, B being Subset of U st Inter (A,B) = {} holds
not A c= B by Th1;