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

A1: 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;

{$} P c= m by Th1;
hence m - ({$} P) = m by A1, Def5; :: thesis: verum