set M = the carrier of L;
for u being object st u in the carrier of L holds
u in the carrier of L ;
then reconsider M = the carrier of L as Subset of L by TARSKI:def 3;
reconsider M = M as non empty Subset of L ;
take M ; :: thesis: ( M is add-closed & M is right-ideal )
thus ( M is add-closed & M is right-ideal ) ; :: thesis: verum