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

proof

let i be set ; :: according to FINSET_1:def 4 :: thesis: ( not i in the carrier of S or the Sorts of T . i is finite )
assume i in the carrier of S ; :: thesis: the Sorts of T . i is finite
hence the Sorts of T . i is finite by A1, FUNCOP_1:13; :: thesis: verum

end;

hence T is finite-yielding by Def11; :: thesis: ( T is non-empty & T is strict )
thus T is non-empty by A1, MSUALG_1:def 8; :: thesis: T is strict
thus T is strict ; :: thesis: verum