let X be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for M being Subset of X
for x being Point of X st x in M holds
0. X in (- x) + M
let M be Subset of X; :: thesis: for x being Point of X st x in M holds
0. X in (- x) + M
let x be Point of X; :: thesis: ( x in M implies 0. X in (- x) + M )
assume x in M ; :: thesis: 0. X in (- x) + M
then (- x) + x in (- x) + M by Lm1;
hence 0. X in (- x) + M by RLVECT_1:5; :: thesis: verum