let V be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; :: thesis: for M, N being Subset of V
for v being Element of V st v in N holds
M - {v} c= M - N
let M, N be Subset of V; :: thesis: for v being Element of V st v in N holds
M - {v} c= M - N
let v be Element of V; :: thesis: ( v in N implies M - {v} c= M - N )
assume A1: v in N ; :: thesis: M - {v} c= M - N
for x being set st x in M - {v} holds
x in M - N

proof

let x be set ; :: thesis: ( x in M - {v} implies x in M - N )
assume A2: x in M - {v} ; :: thesis: x in M - N
then reconsider x = x as Element of V ;
consider u2, v2 being Element of V such that
A3: x = u2 - v2 and
A4: u2 in M and
A5: v2 in {v} by A2;
x = u2 - v by A3, A5, TARSKI:def 1;
hence x in M - N by A1, A4; :: thesis: verum

end;

hence M - {v} c= M - N by TARSKI:def 3; :: thesis: verum