let S be satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: for a, b, c, a9, b9, c9 being POINT of S st between a,b,c & a,b,c cong a9,b9,c9 holds
between a9,b9,c9
let a, b, c, a9, b9, c9 be POINT of S; :: thesis: ( between a,b,c & a,b,c cong a9,b9,c9 implies between a9,b9,c9 )
assume A1: ( between a,b,c & a,b,c cong a9,b9,c9 ) ; :: thesis: between a9,b9,c9
consider b99 being POINT of S such that
A3: ( between a9,b99,c9 & a,b,c cong a9,b99,c9 ) by A1, Satz4p5;
A5: ( a9,b99 equiv a,b & b99,c9 equiv b,c ) by A3, Satz2p2;
then ( a9,b99 equiv a9,b9 & b99,c9 equiv b9,c9 ) by A1, Satz2p3;
then c9,b99 equiv b9,c9 by Satz2p4;
then a9,b99,c9,b99 IFS a9,b99,c9,b9 by A5, A3, A1, Satz2p1, Satz2p3, Satz2p5;
then b99,b9 equiv b99,b99 by Satz2p2, Satz4p2;
hence between a9,b9,c9 by A3, GTARSKI1:def 7; :: thesis: verum