let R be non empty multLoopStr ; :: thesis: for I being non empty right-ideal Subset of
for J being Subset of holds I c= I % J
let I be non empty right-ideal Subset of ; :: thesis: for J being Subset of holds I c= I % J
let J be Subset of ; :: 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 ;

now

let v be set ; :: thesis: ( v in u' * J implies v in I )
assume v in u' * J ; :: thesis: v in I
then ex j being Element of st
( v = u' * j & j in J ) ;
hence v in I by A1, 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