theorem Th45: :: IDEAL_1:45

for L being non empty doubleLoopStr
for I being LeftIdeal of L holds I -LeftIdeal = I by Def15;