IFSC := fun A B C D A' B' C' D' =>
Bet A B C /\ Bet A' B' C' /\
Cong A C A' C' /\ Cong B C B' C' /\
Cong A D A' D' /\ Cong C D C' D'
forall A B C D A' B' C' D', IFSC A B C D A' B' C' D' → Cong B D B' D'
(voir five_segments_with_def - l4_16)
forall A B C A' B' C',
Bet A B C → Bet A' B' C' →
Cong A C A' C' → Cong B C B' C' → Cong A B A' B'
(voir l2_11)
Cong_3 := fun A1 A2 A3 B1 B2 B3 => Cong A1 A2 B1 B2 /\ Cong A1 A3 B1 B3 /\ Cong A2 A3 B2 B3
forall A B C A' C',
Bet A B C → Cong A C A' C' → exists B', Bet A' B' C' /\ Cong_3 A B C A' B' C'
(voir l4_14)
forall A B C A' B' C', Bet A B C → Cong_3 A B C A' B' C' → Bet A' B' C'
(voir l4_13)