:: deftheorem defines AFS GTARSKI3:def 2 :
for S being TarskiGeometryStruct
for a, b, c, d, a9, b9, c9, d9 being POINT of S holds
( a,b,c,d AFS a9,b9,c9,d9 iff ( between a,b,c & between a9,b9,c9 & a,b equiv a9,b9 & b,c equiv b9,c9 & a,d equiv a9,d9 & b,d equiv b9,d9 ) );