let I be non empty Subset of R; :: thesis: ( I is right-ideal implies I is left-ideal )
assume I is right-ideal ; :: thesis: I is left-ideal
then for p, x being Element of R st x in I holds
p * x in I by Def3;
hence I is left-ideal by Def2; :: thesis: verum