theorem Th25: :: INTERVA1:25
for U being non empty set
for A, B being Subset of U st A c= B holds
Inter (A,B) is non empty ordered Subset-Family of U