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 being POINT of S st
( between4 a1,a2,a3,a4 & a1,a2,a3,a4 are_mutually_distinct )
let a1, a2 be POINT of S; :: thesis: ( a1 <> a2 implies ex a3, a4 being POINT of S st
( between4 a1,a2,a3,a4 & a1,a2,a3,a4 are_mutually_distinct ) )
assume a1 <> a2 ; :: thesis: ex a3, a4 being POINT of S st
( between4 a1,a2,a3,a4 & a1,a2,a3,a4 are_mutually_distinct )
then consider a3 being POINT of S such that
A1: ( between a1,a2,a3 & a1,a2,a3 are_mutually_distinct ) by Satz3p15p3;
consider a4 being POINT of S such that
A2: ( between a2,a3,a4 & a2,a3,a4 are_mutually_distinct ) by A1, Satz3p15p3;
take a3 ; :: thesis: ex a4 being POINT of S st
( between4 a1,a2,a3,a4 & a1,a2,a3,a4 are_mutually_distinct )
take a4 ; :: thesis: ( between4 a1,a2,a3,a4 & a1,a2,a3,a4 are_mutually_distinct )
thus between4 a1,a2,a3,a4 by A1, A2, Satz3p7p1, Satz3p7p2; :: thesis: a1,a2,a3,a4 are_mutually_distinct
thus a1,a2,a3,a4 are_mutually_distinct by A1, Satz3p7p1, GTARSKI1:def 10, A2; :: thesis: verum