theorem :: IDEAL_1:56

for L being non empty doubleLoopStr holds ([#] L) -RightIdeal = the carrier of L by Def16;