let S be satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct ; :: thesis: for a1, a2 being POINT of S st a1 <> a2 holds
ex a3, a4, a5 being POINT of S st
( between5 a1,a2,a3,a4,a5 & a1,a2,a3,a4,a5 are_mutually_distinct )
let a1, a2 be POINT of S; :: thesis: ( a1 <> a2 implies ex a3, a4, a5 being POINT of S st
( between5 a1,a2,a3,a4,a5 & a1,a2,a3,a4,a5 are_mutually_distinct ) )
assume a1 <> a2 ; :: thesis: ex a3, a4, a5 being POINT of S st
( between5 a1,a2,a3,a4,a5 & a1,a2,a3,a4,a5 are_mutually_distinct )
then consider a3, a4 being POINT of S such that
A1: ( between4 a1,a2,a3,a4 & a1,a2,a3,a4 are_mutually_distinct ) by Satz3p15p4;
consider a5 being POINT of S such that
A2: ( between a3,a4,a5 & a3,a4,a5 are_mutually_distinct ) by A1, Satz3p15p3;
take a3 ; :: thesis: ex a4, a5 being POINT of S st
( between5 a1,a2,a3,a4,a5 & a1,a2,a3,a4,a5 are_mutually_distinct )
take a4 ; :: thesis: ex a5 being POINT of S st
( between5 a1,a2,a3,a4,a5 & a1,a2,a3,a4,a5 are_mutually_distinct )
take a5 ; :: thesis: ( between5 a1,a2,a3,a4,a5 & a1,a2,a3,a4,a5 are_mutually_distinct )
( between a1,a3,a5 & between a1,a4,a5 & between a2,a3,a5 & between a2,a4,a5 ) by A1, A2, Satz3p7p1, Satz3p7p2;
hence between5 a1,a2,a3,a4,a5 by A1, A2, Satz3p6p2; :: thesis: a1,a2,a3,a4,a5 are_mutually_distinct
thus a1,a2,a3,a4,a5 are_mutually_distinct by A1, A2, Satz3p7p1, GTARSKI1:def 10; :: thesis: verum