let X be non empty right_zeroed addLoopStr ; :: thesis: for V1, V2 being Subset of X st 0. X in V2 holds
V1 c= V1 + V2
let V1, V2 be Subset of X; :: thesis: ( 0. X in V2 implies V1 c= V1 + V2 )
assume A1: 0. X in V2 ; :: thesis: V1 c= V1 + V2
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in V1 or x in V1 + V2 )
assume A2: x in V1 ; :: thesis: x in V1 + V2
then reconsider x = x as Point of X ;
x + (0. X) = x by RLVECT_1:def 4;
then x in { (u + v) where u, v is Point of X : ( u in V1 & v in V2 ) } by A1, A2;
hence x in V1 + V2 by RUSUB_4:def 9; :: thesis: verum