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

proof

let x, y be Element of L; :: according to IDEAL_1:def 2 :: thesis: ( y in cL implies x * y in cL )
thus ( y in cL implies x * y in cL ) ; :: thesis: verum

end;

A2: cL is right-ideal

proof

let x, y be Element of L; :: according to IDEAL_1:def 3 :: thesis: ( y in cL implies y * x in cL )
thus ( y in cL implies y * x in cL ) ; :: thesis: verum

end;

cL is add-closed

proof

let x, y be Element of L; :: according to IDEAL_1:def 1 :: thesis: ( x in cL & y in cL implies x + y in cL )
thus ( x in cL & y in cL implies x + y in cL ) ; :: thesis: verum

end;

hence the carrier of L is Ideal of L by A1, A2; :: thesis: verum