:: deftheorem defines /\ IDEAL_1:def 20 :
for R being non empty 1-sorted
for I, J being Subset of R holds I /\ J = { x where x is Element of R : ( x in I & x in J ) } ;