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

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