let S be non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct ; :: thesis: for a, b, c being POINT of S
for A being Subset of S st A out a,b & A out b,c holds
A out a,c
let a, b, c be POINT of S; :: thesis: for A being Subset of S st A out a,b & A out b,c holds
A out a,c
let A be Subset of S; :: thesis: ( A out a,b & A out b,c implies A out a,c )
assume that
A1: A out a,b and
A2: A out b,c ; :: thesis: A out a,c
consider x being POINT of S such that
A3: between a,A,x and
A4: between b,A,x by A1;
consider y being POINT of S such that
A5: between b,A,y and
A6: between c,A,y by A2;
( between x,A,b & between y,A,b ) by A4, A5, GTARSKI3:14;
then ( between y,A,c & A out y,x ) by A6, GTARSKI3:14;
then between x,A,c by Th14;
then between c,A,x by GTARSKI3:14;
hence A out a,c by A3; :: thesis: verum