Propriétés de le

Definition le

le := fun A B C D => exists y, Bet C y D /\ Cong A B C y

Sorry, the GeoGebra Applet could not be started. Please make sure that Java 1.4.2 (or later) is installed and active in your browser (Click here to install Java now)

Definition ge

ge := fun A B C D => le C D A B

l5_1

forall A B C D : Point, A ≠ B → Bet A B C → Bet A B D → Bet A C D \/ Bet A D C

l5_2

forall A B C D : Point, A ≠ B → Bet A B C → Bet A B D → Bet B C D \/ Bet B D C

l5_3

forall A B C D : Point, Bet A B D → Bet A C D → Bet A B C \/ Bet A C B

l5_5_1

forall A B C D : Point, le A B C D → exists x, Bet A B x /\ Cong A x C D

Sorry, the GeoGebra Applet could not be started. Please make sure that Java 1.4.2 (or later) is installed and active in your browser (Click here to install Java now)

l5_5_2 (réciproque)

forall A B C D, (exists x, Bet A B x /\ Cong A x C D) → le A B C D

l5_6

forall A B C D A' B' C' D', le A B C D /\ Cong A B A' B' /\ Cong C D C' D' → le A' B' C' D'

Sorry, the GeoGebra Applet could not be started. Please make sure that Java 1.4.2 (or later) is installed and active in your browser (Click here to install Java now)

le_reflexivity

forall A B, le A B A B

le_transitivity

forall A B C D E F, le A B C D → le C D E F → le A B E F

between_cong

forall A B C, Bet A C B → Cong A C A B → C=B

between_cong_2

forall A B D E, Bet A D B → Bet A E B → Cong A D A E → D = E

le_anti_symmetry

forall A B C D, le A B C D → le C D A B → Cong A B C D

segment_construction_2

forall A Q B C, A ≠ Q → exists X, (Bet Q A X \/ Bet Q X A) /\ Cong Q X B C

Sorry, the GeoGebra Applet could not be started. Please make sure that Java 1.4.2 (or later) is installed and active in your browser (Click here to install Java now)

le_trivial

forall A C D, le A A C D

le_cases

forall A B C D : Point, le A B C D \/ le C D A B

le_zero

forall A B C, le A B C C → A = B

Definition lt

lt := fun A B C D => le A B C D /\ ~ Cong A B C D

Definition gt

gt := fun A B C D => lt C D A B.