theorem :: INTERVA1:49

for U being non empty set ex A being non empty IntervalSet of U st (A _/\_ A) ^ <> Inter (({} U),({} U))