deffunc H₁( set ) -> Element of NAT = ($1 multitude_of ) -' ($1 multitude_of );
consider m being marking of P such that
A2: 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 A3: p in P ; :: thesis: p multitude_of = (p multitude_of ) - (p multitude_of )
then A4: p multitude_of >= p multitude_of by A1, Def4;
thus p multitude_of = (p multitude_of ) -' (p multitude_of ) by A2, A3
.= (p multitude_of ) - (p multitude_of ) by A4, XREAL_1:235 ; :: thesis: verum