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 u' = u as Element of R ;

now

let v be set ; :: thesis: ( v in u' * J implies v in I )
assume v in u' * J ; :: thesis: v in I
then consider j being Element of R such that
A2: ( v = u' * j & j in J ) ;
thus v in I by A1, A2, Def3; :: thesis: verum

end;

then u' * 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