deffunc H₁( set ) -> Element of NAT = ($1 multitude_of ) -' ($1 multitude_of );
consider m being marking of P such that
A1: for p being set st p in P holds
p multitude_of = H₁(p) from PNPROC_1:sch 1();
take m ; :: thesis: for p being set st p in P holds
p multitude_of = (p multitude_of ) - (p multitude_of )
let p be set ; :: thesis: ( p in P implies p multitude_of = (p multitude_of ) - (p multitude_of ) )
assume A2: p in P ; :: thesis: p multitude_of = (p multitude_of ) - (p multitude_of )
then A3: p multitude_of >= p multitude_of by B1, Def3;
thus p multitude_of = (p multitude_of ) -' (p multitude_of ) by A1, A2
.= (p multitude_of ) - (p multitude_of ) by A3, XREAL_1:233 ; :: thesis: verum