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

now :: thesis: for p being set st p in P holds
m . 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;

hence m + ({$} P) = m by Def4; :: thesis: verum