:: deftheorem defines | MYCIELSK:def 1 :
for X being set
for P being a_partition of X
for S being Subset of X holds P | S = { (x /\ S) where x is Element of P : x meets S } ;