let L be non empty well-unital doubleLoopStr ; :: thesis: {(1. L)} -Ideal = the carrier of L
the carrier of L c= {(1. L)} -Ideal

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of L or x in {(1. L)} -Ideal )
assume x in the carrier of L ; :: thesis: x in {(1. L)} -Ideal
then reconsider x9 = x as Element of L ;
( 1. L in {(1. L)} & {(1. L)} c= {(1. L)} -Ideal ) by Def14, TARSKI:def 1;
then x9 * (1. L) in {(1. L)} -Ideal by Def2;
hence x in {(1. L)} -Ideal ; :: thesis: verum

end;

hence {(1. L)} -Ideal = the carrier of L ; :: thesis: verum