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

now

let u be set ; :: thesis: ( u in I implies u in I % J )
assume A1: u in I ; :: thesis: u in I % J
then reconsider u9 = u as Element of R ;

now

let v be set ; :: 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 by TARSKI:def 3;
hence u in I % J ; :: thesis: verum

end;

hence I c= I % J by TARSKI:def 3; :: thesis: verum