let L be non empty doubleLoopStr ; :: thesis: ([#] L) -Ideal = the carrier of L
[#] L c= ([#] L) -Ideal by Def15;
hence ([#] L) -Ideal = the carrier of L by XBOOLE_0:def 10; :: thesis: verum