theorem :: IDEAL_1:54

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