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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of L or x in {(1. L)} -RightIdeal )
assume x in the carrier of L ; :: thesis: x in {(1. L)} -RightIdeal
then reconsider x9 = x as Element of L ;
( 1. L in {(1. L)} & {(1. L)} c= {(1. L)} -RightIdeal ) by Def17, TARSKI:def 1;
then (1. L) * x9 in {(1. L)} -RightIdeal by Def3;
hence x in {(1. L)} -RightIdeal by VECTSP_1:def 8; :: thesis: verum

end;

hence {(1. L)} -RightIdeal = the carrier of L by XBOOLE_0:def 10; :: thesis: verum