consider z being non empty set , CH being ManySortedFunction of ((ConstOSSet (S,z)) #) * the Arity of S,(ConstOSSet (S,z)) * the ResultSort of S;
take ConstOSA (S,z,CH) ; :: thesis: ( ConstOSA (S,z,CH) is strict & ConstOSA (S,z,CH) is non-empty & ConstOSA (S,z,CH) is order-sorted )
thus ( ConstOSA (S,z,CH) is strict & ConstOSA (S,z,CH) is non-empty & ConstOSA (S,z,CH) is order-sorted ) by Th18; :: thesis: verum