let L be non empty doubleLoopStr ; :: thesis: for I being Ideal of L holds I -Ideal = I
let I be Ideal of L; :: thesis: I -Ideal = I
( I c= I -Ideal & I -Ideal c= I ) by Def15;
hence I -Ideal = I by XBOOLE_0:def 10; :: thesis: verum