let S be satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: for a, b, c, p, a9, b9, c9 being POINT of S st between a,b,c & between a9,b9,c & between a,p,a9 holds
ex q being POINT of S st
( between p,q,c & between b,q,b9 )
let a, b, c, p, a9, b9, c9 be POINT of S; :: thesis: ( between a,b,c & between a9,b9,c & between a,p,a9 implies ex q being POINT of S st
( between p,q,c & between b,q,b9 ) )
assume A1: ( between a,b,c & between a9,b9,c & between a,p,a9 ) ; :: thesis: ex q being POINT of S st
( between p,q,c & between b,q,b9 )
then between c,b9,a9 by Satz3p2;
then consider x being POINT of S such that
A2: ( between b9,x,a & between p,x,c ) by A1, GTARSKI1:def 11;
between c,b,a by A1, Satz3p2;
then consider q being POINT of S such that
A3: ( between x,q,c & between b,q,b9 ) by A2, GTARSKI1:def 11;
between p,q,c by A2, A3, Satz3p5p2;
hence ex q being POINT of S st
( between p,q,c & between b,q,b9 ) by A3; :: thesis: verum