let L be non empty doubleLoopStr ; :: thesis: the carrier of L is Ideal 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 left-ideal ;
A2: cL is right-ideal ;
cL is add-closed ;
hence the carrier of L is Ideal of L by A1, A2; :: thesis: verum