theorem Th11: :: IDEAL_1:11

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