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

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 Lm6;
hence m . p = (m . p) - (({$} P) . p) ; :: thesis: verum

end;

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