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