for L being non empty doubleLoopStr
for I being Ideal of L holds I -Ideal = I by Def14;