thus the Sorts of (Trivial_Algebra S) is finite-yielding ; :: according to MSAFREE2:def 11 :: thesis: Trivial_Algebra S is non-empty
let i be set ; :: according to MSUALG_1:def 8,PBOOLE:def 16 :: thesis: ( not i in the carrier of S or not the Sorts of (Trivial_Algebra S) . i is empty )
assume i in the carrier of S ; :: thesis: not the Sorts of (Trivial_Algebra S) . i is empty
hence not the Sorts of (Trivial_Algebra S) . i is empty ; :: thesis: verum