let S be satisfying_A8 TarskiGeometryStruct ; not for a, b, c being POINT of S holds Collinear a,b,c
consider a, b, c being POINT of S such that
A1:
not between a,b,c
and
A2:
not between b,c,a
and
A3:
not between c,a,b
by GTARSKI2:def 7;
not Collinear a,b,c
by A1, A2, A3;
hence
not for a, b, c being POINT of S holds Collinear a,b,c
; verum