theorem :: INTERVA1:51

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