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