:: deftheorem defines '/\' PARTIT1:def 4 :
for Y being non empty set
for PA, PB being a_partition of Y holds PA '/\' PB = (INTERSECTION (PA,PB)) \ {{}};