set A = {0 };
consider a being BinOp of {0 };
reconsider z = 0 as Element of {0 } by TARSKI:def 1;
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:57;
take B = AlgebraStr(# {0 },a,a,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