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;
thus T is finite-yielding :: thesis: ( T is non-empty & T is strict )

proof

thus the Sorts of T is finite-yielding :: according to MSAFREE2:def 11 :: thesis: verum

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;

end;

thus T is non-empty :: thesis: T is strict

proof

thus the Sorts of T is non-empty by A1; :: according to MSUALG_1:def 8 :: thesis: verum

end;

thus T is strict ; :: thesis: verum