let R be non empty right_add-cancelable right_zeroed right-distributive left_zeroed doubleLoopStr ; :: thesis: for I, J being non empty right-ideal Subset of R holds I c= I + J
let I, J be non empty right-ideal Subset of R; :: thesis: I c= I + J
let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in I or u in I + J )
assume u in I ; :: thesis: u in I + J
then reconsider u9 = u as Element of I ;
0. R is Element of J by Th3;
then u9 + (0. R) in { (a + b) where a, b is Element of R : ( a in I & b in J ) } ;
hence u in I + J by RLVECT_1:def 4; :: thesis: verum