let I be non empty Subset of ; :: 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 st x in I holds
p * x in I by Def3;
hence I is left-ideal by Def2; :: thesis: verum