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