Аксиомы

Для любых двух точек A и B отрезок AB конгруэнтен отрезку BA. Это исходное свойство отношения конгруэнтности, из которого впоследствии выводятся его симметрия и рефлексивность.

axiomatization where
  congr_pseudo_refl:
    "\<And>A B. Congr A B B A"

Если отрезки C D и E F конгруэнтны отрезку A B, то они конгруэнтны друг другу.

axiomatization where
  congr_inner_transitivity:
    "\<And>A B C D E F.
       Congr A B C D \<Longrightarrow>
       Congr A B E F \<Longrightarrow>
       Congr C D E F"

Если отрезок AB конгруэнтен вырожденному отрезку CC, то A и B совпадают.

axiomatization where
  congr_id:
    "\<And>A B C.
       Congr A B C C \<Longrightarrow>
       A = B"

Если Bet A B A, то A = B

axiomatization where
  bet_id:
    "\<And>A B.
       Bet A B A \<Longrightarrow>
       A = B"

Если P лежит между A и C, а Q — между B и C, то отрезки P B и Q A пересекаются в некоторой точке X.

axiomatization where
  inner_pasch:
    "\<And>A B C P Q.
       Bet A P C \<Longrightarrow>
       Bet B Q C \<Longrightarrow>
       \<exists>X.
         Bet P X B \<and>
         Bet Q X A"

axiomatization where
  five_segment:
    "\<And>A A' B B' C C' D D'.
       Congr A B A' B' \<Longrightarrow>
       Congr B C B' C' \<Longrightarrow>
       Congr A D A' D' \<Longrightarrow>
       Congr B D B' D' \<Longrightarrow>
       Bet A B C \<Longrightarrow>
       Bet A' B' C' \<Longrightarrow>
       A \<noteq> B \<Longrightarrow>
       Congr C D C' D'"