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
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in M - {v} or 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