take ConstOSSet (R,1) ; :: thesis: ConstOSSet (R,1) is non-empty
thus ConstOSSet (R,1) is non-empty by Th15; :: thesis: verum