theorem :: IDEAL_1:58

for L being non empty doubleLoopStr
for A, B being non empty Subset of L st A c= B holds
A -LeftIdeal c= B -LeftIdeal