theorem Th12: :: IDEAL_1:12

for L being non empty doubleLoopStr holds the carrier of L is RightIdeal of L