-- hets -g Calculi/Space/RCCVerification.dol von CASL-Lib aus aufrufen!

-- Bei SPASS-Beweisen: C_-Axiome abwählen, bei ExtRCCByRCC8Rels C_sym
   und C_nonnull drinlassen, bei ExtRCC_FO vs. RCC_FO auch C_id
   Letzterer ist gut für Demo, da schnell! (Ersterer dagegen langsam,
   Rest braucht Bridge Lemmas nicht.)

-- Timelimit: 40 reicht durchweg

-- Isabelle-Beweis: [simp] dazu bei Field_unary_minus_def,
   Real_divide_def, Real_half_def;
   [simp] weg bei half_gt_zero.