let L be non empty doubleLoopStr ; :: thesis: the carrier of L is RightIdeal of L
the carrier of L c= the carrier of L ;
then reconsider cL = the carrier of L as Subset of L ;
A1: cL is right-ideal ;
cL is add-closed ;
hence the carrier of L is RightIdeal of L by A1; :: thesis: verum