theorem :: INTERVA1:47

for U being non empty set holds (Inter (({} U),({} U))) ^ = Inter (([#] U),([#] U))