reconsider b = AlgebraStr(# the carrier of B,the addF of B,the multF of B,(0. B),(1. B),the lmult of B #) as Subalgebra of B by Th14;
take b ; :: thesis: b is strict
thus b is strict ; :: thesis: verum