let P be set ; :: thesis: for m being marking of P holds m + ({$} P) = m

let m be marking of P; :: thesis: m + ({$} P) = m

let m be marking of P; :: thesis: m + ({$} P) = m

now :: thesis: for p being set st p in P holds

m . p = (m . p) + (({$} P) . p)

hence
m + ({$} P) = m
by Def4; :: thesis: verumm . p = (m . p) + (({$} P) . p)

let p be set ; :: thesis: ( p in P implies m . p = (m . p) + (({$} P) . p) )

assume p in P ; :: thesis: m . p = (m . p) + (({$} P) . p)

then ({$} P) . p = 0 by Lm1;

hence m . p = (m . p) + (({$} P) . p) ; :: thesis: verum

end;assume p in P ; :: thesis: m . p = (m . p) + (({$} P) . p)

then ({$} P) . p = 0 by Lm1;

hence m . p = (m . p) + (({$} P) . p) ; :: thesis: verum