let R be non empty multLoopStr ; :: thesis: for I being non empty right-ideal Subset of R
for J being Subset of R holds I c= I % J
let I be non empty right-ideal Subset of R; :: thesis: for J being Subset of R holds I c= I % J
let J be 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 A1: u in I ; :: thesis: u in I % J
then reconsider u9 = u as Element of R ;
now :: thesis: for v being object st v in u9 * J holds
v in I
let v be object ; :: thesis: ( v in u9 * J implies v in I )
assume v in u9 * J ; :: thesis: v in I
then ex j being Element of R st
( v = u9 * j & j in J ) ;
hence v in I by A1, Def3; :: thesis: verum
end;
then u9 * J c= I ;
hence u in I % J ; :: thesis: verum