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