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