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

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

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)

{$} P c= m
by Th1;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;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

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