let P be set ; :: thesis: for m1, m2 being marking of P st m1 c= m2 & m2 c= m1 holds
m1 = m2
let m1, m2 be marking of P; :: thesis: ( m1 c= m2 & m2 c= m1 implies m1 = m2 )
assume A1: m1 c= m2 ; :: thesis: ( not m2 c= m1 or m1 = m2 )
assume A2: m2 c= m1 ; :: thesis: m1 = m2
let p be object ; :: according to PNPROC_1:def 1 :: thesis: ( p in P implies p multitude_of = p multitude_of )
assume A3: p in P ; :: thesis: p multitude_of = p multitude_of
then A4: m1 . p <= m2 . p by A1;
m2 . p <= m1 . p by A2, A3;
hence p multitude_of = p multitude_of by A4, XXREAL_0:1; :: thesis: verum