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 = the BinOp of {0};
take AlgebraStr(# {0}, the BinOp of {0}, the BinOp of {0},z,z,lm #) ; :: thesis: ( AlgebraStr(# {0}, the BinOp of {0}, the BinOp of {0},z,z,lm #) is strict & not AlgebraStr(# {0}, the BinOp of {0}, the BinOp of {0},z,z,lm #) is empty )
thus ( AlgebraStr(# {0}, the BinOp of {0}, the BinOp of {0},z,z,lm #) is strict & not AlgebraStr(# {0}, the BinOp of {0}, the BinOp of {0},z,z,lm #) is empty ) ; :: thesis: verum