let P be set ; :: thesis: for m1, m2, m3 being marking of P st m1 c= m2 & m2 c= m3 holds
m1 c= m3
let m1, m2, m3 be marking of P; :: thesis: ( m1 c= m2 & m2 c= m3 implies m1 c= m3 )
assume A1: ( m1 c= m2 & m2 c= m3 ) ; :: thesis: m1 c= m3
let p be set ; :: according to PNPROC_1:def 4 :: thesis: ( p in P implies p multitude_of <= p multitude_of )
assume p in P ; :: thesis: p multitude_of <= p multitude_of
then ( m1 . p <= m2 . p & m2 . p <= m3 . p ) by A1, Def4;
hence m1 . p <= m3 . p by XXREAL_0:2; :: thesis: verum