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