0 in {0} by TARSKI:def 1;
then reconsider lm = [: the carrier of L,{0}:] --> 0 as Function of [: the carrier of L,{0}:],{0} by FUNCOP_1:45;
reconsider z = 0 as Element of {0} by TARSKI:def 1;
set A = {0};
set a = the BinOp of {0};
take B = AlgebraStr(# {0}, the BinOp of {0}, the BinOp of {0},z,z,lm #); :: thesis: ( not B is empty & B is strict )
thus not B is empty ; :: thesis: B is strict
thus B is strict ; :: thesis: verum