set z = the non empty set ;
take ConstOSSet (R, the non empty set ) ; :: thesis: ConstOSSet (R, the non empty set ) is order-sorted
thus ConstOSSet (R, the non empty set ) is order-sorted by Th16; :: thesis: verum