for i being object st i in the carrier of S holds
not (ConstOSSet (S,z)) . i is empty by FUNCOP_1:7;
then ConstOSSet (S,z) is V8() by PBOOLE:def 13;
then reconsider T = MSAlgebra(# (ConstOSSet (S,z)),CH #) as strict non-empty MSAlgebra over S by MSUALG_1:def 3;
take T ; :: thesis: ( the Sorts of T = ConstOSSet (S,z) & the Charact of T = CH )
thus ( the Sorts of T = ConstOSSet (S,z) & the Charact of T = CH ) ; :: thesis: verum