let S be satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_BetweennessIdentity satisfying_Pasch TarskiGeometryStruct ; :: thesis: for a, b, c being POINT of S st ( Middle a,b,c or between a,b,c ) holds
( Collinear a,b,c & Collinear b,c,a & Collinear c,a,b & Collinear c,b,a & Collinear b,a,c & Collinear a,c,b )
let a, b, c be POINT of S; :: thesis: ( ( Middle a,b,c or between a,b,c ) implies ( Collinear a,b,c & Collinear b,c,a & Collinear c,a,b & Collinear c,b,a & Collinear b,a,c & Collinear a,c,b ) )
assume ( Middle a,b,c or between a,b,c ) ; :: thesis: ( Collinear a,b,c & Collinear b,c,a & Collinear c,a,b & Collinear c,b,a & Collinear b,a,c & Collinear a,c,b )
then Collinear a,b,c by Prelim08;
hence ( Collinear a,b,c & Collinear b,c,a & Collinear c,a,b & Collinear c,b,a & Collinear b,a,c & Collinear a,c,b ) by GTARSKI3:45; :: thesis: verum