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

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