Propriétés de two_sides

Definition two_sides

two_sides := fun A B P Q => A<>B /\ ~ Col P A B /\ ~ Col Q A B /\ exists T, Col T A B /\ Bet P T Q

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)

l9_2 (symmetry)

forall A B P Q, two_sides A B P Q → two_sides A B Q P

inter_unicity

forall A B X Y M N,
Col A B M→ Col X Y M → Col A B N → Col X Y N → ~ Col A X B → X <> Y → M = N

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)

l9_3

forall P Q A C M R B,
two_sides P Q A C → Col M P Q → is_midpoint M A C → Col R P Q → out R A B →
two_sides P Q 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)

l9_4_1

forall P Q A C R S M,
two_sides P Q A C
→ Col R P Q → Perp P Q A R
→ Col S P Q → Perp P Q C S
→ is_midpoint M R S → (forall U V, is_midpoint M U V → (out R U A ↔ out S C V))

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)

l9_4_2

forall P Q A C R S U V,
two_sides P Q A C
→ Col R P Q → Perp P Q A R
→ Col S P Q → Perp P Q C S
→ out R U A → out S V C → two_sides P Q U V

l9_5

forall P Q A C R B, two_sides P Q A C → Col R P Q → out R A B → two_sides P Q 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)

outer_pash

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

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 : one_side

one_side := fun P Q A B => exists C, two_sides P Q A C /\ two_sides P Q 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)

l9_8_2

forall P Q A B C, two_sides P Q A C → one_side P Q A B → two_sides P Q B C

l9_9

forall P Q A B, two_sides P Q A B → ~ one_side P Q A B

l9_9_bis

forall P Q A B, one_side P Q A B → ~ two_sides P Q A B

l9_10

forall P Q A, P ≠ Q → ~ Col A P Q → exists C, two_sides P Q A C

one_side_reflexivity

forall P Q A, ~ Col A P Q → one_side P Q A A

one_side_symmetry

forall P Q A B, one_side P Q A B → one_side P Q B A

one_side_transitivity

forall P Q A B C, one_side P Q A B → one_side P Q B C → one_side P Q A C