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

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