:: deftheorem defines Inter INTERVA1:def 1 :
for U being set
for X, Y being Subset of U holds Inter (X,Y) = { A where A is Subset of U : ( X c= A & A c= Y ) } ;