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