theorem :: INTERVA1:48

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