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