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