let L be non empty right_zeroed addLoopStr ; :: thesis: {(0. L)} is add-closed
let x, y be Element of L; :: according to IDEAL_1:def 1 :: thesis: ( x in {(0. L)} & y in {(0. L)} implies x + y in {(0. L)} )
assume ( x in {(0. L)} & y in {(0. L)} ) ; :: thesis: x + y in {(0. L)}
then ( x = 0. L & y = 0. L ) by TARSKI:def 1;
then x + y = 0. L by RLVECT_1:def 4;
hence x + y in {(0. L)} by TARSKI:def 1; :: thesis: verum