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