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