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