theorem :: IDEAL_1:55

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