set M = { x where x is Element of R : ( x in I & x in J ) } ;
{ x where x is Element of R : ( x in I & x in J ) } = I /\ J ;
then reconsider M = { x where x is Element of R : ( x in I & x in J ) } as Subset of R ;
for y, x being Element of R st x in M holds
x * y in M

proof

let y, x be Element of R; :: thesis: ( x in M implies x * y in M )
assume x in M ; :: thesis: x * y in M
then consider a being Element of R such that
A1: x = a and
A2: ( a in I & a in J ) ;
( a * y in I & a * y in J ) by A2, Def3;
hence x * y in M by A1; :: thesis: verum

end;

hence for b₁ being Subset of R st b₁ = I /\ J holds
b₁ is right-ideal ; :: thesis: verum