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