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