consider z being non empty set ;
take ConstOSSet R,z ; :: thesis: ConstOSSet R,z is order-sorted
thus ConstOSSet R,z is order-sorted by Th16; :: thesis: verum