theorem Th46: :: IDEAL_1:46
for L being non empty doubleLoopStr
for I being RightIdeal of L holds I -RightIdeal = I by Def16;