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