let S be satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: for a, b, o being POINT of S st o <> a holds
ex x, y being POINT of S st
( between b,o,x & between a,o,y & x,y,o cong a,b,o )
let a, b, o be POINT of S; :: thesis: ( o <> a implies ex x, y being POINT of S st
( between b,o,x & between a,o,y & x,y,o cong a,b,o ) )
assume X1: o <> a ; :: thesis: ex x, y being POINT of S st
( between b,o,x & between a,o,y & x,y,o cong a,b,o )
consider x being POINT of S such that
X2: ( between b,o,x & o,x equiv o,a ) by A4;
x,o equiv a,o by X2, CongruenceDoubleSymmetry;
then X5: a,o,x cong x,o,a by X2, A1, EquivSymmetric;
consider y being POINT of S such that
X6: ( between a,o,y & o,y equiv o,b ) by A4;
between x,o,b by X2, Bsymmetry;
then x,y,o cong a,b,o by X6, CongruenceDoubleSymmetry, X1, X5, A5;
hence ex x, y being POINT of S st
( between b,o,x & between a,o,y & x,y,o cong a,b,o ) by X2, X6; :: thesis: verum