let L be non empty right_zeroed addLoopStr ; :: thesis: for S, T being Subset of L st 0. L in T holds
S c= S + T
let S, T be Subset of L; :: thesis: ( 0. L in T implies S c= S + T )
assume A: 0. L in T ; :: thesis: S c= S + T
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in S or x in S + T )
assume B: x in S ; :: thesis: x in S + T
then reconsider a = x as Element of L ;
a + (0. L) in { (c + b) where c, b is Element of L : ( c in S & b in T ) } by A, B;
hence x in S + T by RLVECT_1:def 4; :: thesis: verum