theorem Th2: :: PNPROC_1:2

for P being set
for m1, m2, m3 being marking of P st m1 c= m2 & m2 c= m3 holds
m1 c= m3