take T = Trivial_Algebra S; :: thesis: ( T is finite-yielding & T is non-empty & T is strict )
A1: the Sorts of T = the carrier of S --> {0} by Def12;
the Sorts of T is finite-yielding by A1, FUNCOP_1:7;
hence T is finite-yielding ; :: thesis: ( T is non-empty & T is strict )
thus T is non-empty by A1; :: thesis: T is strict
thus T is strict ; :: thesis: verum