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 out2 a,b & A out2 b,c holds
A out2 a,c
let a, b, c be POINT of S; :: thesis: for A being Subset of S st A out2 a,b & A out2 b,c holds
A out2 a,c
let A be Subset of S; :: thesis: ( A out2 a,b & A out2 b,c implies A out2 a,c )
assume that
A1: A out2 a,b and
A2: A out2 b,c ; :: thesis: A out2 a,c
consider x being POINT of S such that
A3: between2 a,A,x and
A4: between2 b,A,x by A1;
consider y being POINT of S such that
A5: between2 b,A,y and
A6: between2 c,A,y by A2;
( between2 x,A,b & between2 y,A,b ) by A4, A5, GTARSKI3:14;
then ( between2 y,A,c & A out2 y,x ) by A6, GTARSKI3:14;
then between2 x,A,c by Th74;
then between2 c,A,x by GTARSKI3:14;
hence A out2 a,c by A3; :: thesis: verum