proposition: Lemma lower_dim_B : ~ T PC PA PB /\ ~ T PA PC PB /\ ~ T PA PB PC.
proof: Proof. assert (HNBet := lower_dim). elim (T_dec PC PA PB); intro HT1; elim (T_dec PA PC PB); intro HT2; elim (T_dec PA PB PC); intro HT3. exfalso; apply HNBet; left; apply T_Bet; assumption. exfalso; apply HNBet; right; right; apply T_Bet; assumption. exfalso; apply HNBet; left; apply T_Bet; assumption. exfalso; apply HNBet; right; right; apply T_Bet; assumption. exfalso; apply HNBet; left; apply T_Bet; assumption. exfalso; apply HNBet; right; left; apply between_symmetry; apply T_Bet; assumption. exfalso; apply HNBet; left; apply T_Bet; assumption. tauto. Qed.
imports: GeoCoq.Axioms.beeson_s_axioms GeoCoq.Tarski_dev.Ch08_orthogonality