theorem Th11: :: PNPROC_1:11

for P being set
for m1, m2, m3 being marking of P holds (m1 + m2) + m3 = m1 + (m2 + m3)