let S be satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: for a, b, c, r being POINT of S st r <> a & b <> c holds
ex x being POINT of S st
( a out x,r & a,x equiv b,c )
let a, b, c, r be POINT of S; :: thesis: ( r <> a & b <> c implies ex x being POINT of S st
( a out x,r & a,x equiv b,c ) )
assume A1: ( r <> a & b <> c ) ; :: thesis: ex x being POINT of S st
( a out x,r & a,x equiv b,c )
consider x being POINT of S such that
A2: ( ( between a,r,x or between a,x,r ) & a,x equiv b,c ) by Lemmapsegcon2;
a out x,r by A1, A2, Satz2p2, GTARSKI1:def 7;
hence ex x being POINT of S st
( a out x,r & a,x equiv b,c ) by A2; :: thesis: verum