theorem Th1: :: INTERVA1:1
for U being set
for X, Y being Subset of U
for x being set holds
( x in Inter (X,Y) iff ( X c= x & x c= Y ) )