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