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 ;
hence I is left-ideal ; :: thesis: verum