set M = the carrier of L;
for u being set st u in the carrier of L holds
u in the carrier of L ;
then reconsider M = the carrier of L as Subset of by TARSKI:def 3;
reconsider M = M as non empty Subset of ;
take M ; :: thesis: ( M is add-closed & M is right-ideal )
( ( for x, y being Element of st x in M & y in M holds
x + y in M ) & ( for p, x being Element of st x in M holds
x * p in M ) ) ;
hence ( M is add-closed & M is right-ideal ) by Def1, Def3; :: thesis: verum