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 & not b is empty )
thus ( b is strict & not b is empty ) ; :: thesis: verum