theorem :: INTERVA1:9

for U being non empty set holds {} is IntervalSet of U