assume RelOb C is empty ; :: thesis: contradiction
then dom (RelOb C) = {} ;
hence contradiction by Th34; :: thesis: verum