Propriétés de between

beetween_trivial

forall A B : Point, Bet A B B

between_symmetry

forall A B C : Point, Bet A B C → Bet C B A

beetween_trivial2

forall A B : Point, Bet A A B

between_egality

forall A B C : Point, Bet A B C → Bet B A C → A = B

between_inner_transitivity

forall A B C D, Bet A B D → Bet B C D → Bet A B C

between_exchange3

forall A B C D, Bet A B C → Bet A C D → Bet B C D

outer_transitivity_between2

forall A B C D, Bet A B C → Bet B C D → B<>C → Bet A C D

between_exchange2

forall A B C D, Bet A B D → Bet B C D → Bet A C D

outer_transitivity_between

forall A B C D, Bet A B C → Bet B C D → B<>C → Bet A B D

between_exchange4

forall A B C D, Bet A B C → Bet A C D → Bet A B D

Définition : Bet4

Bet_4 := fun A1 A2 A3 A4 =>
Bet A1 A2 A3 /\ Bet A2 A3 A4 /\ Bet A1 A3 A4 /\ Bet A1 A2 A4

l_3_9_4

forall A1 A2 A3 A4, Bet_4 A1 A2 A3 A4 → Bet_4 A4 A3 A2 A1

two_distinct_points

exists x, exists y, x <> y

point_construction_different

forall A B, exists C, Bet A B C /\ B <> C

another_point

forall A, exists B, A<>B

l3_17

forall A B C A' B' P,
Bet A B C → Bet A' B' C → Bet A P A' →
exists Q, Bet P Q C /\ Bet B Q B'