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