:: deftheorem defines Krippenfigur GTARSKI3:def 14 :
for S being TarskiGeometryStruct
for a1, a2, b1, b2, c, m1, m2 being POINT of S holds
( Krippenfigur a1,m1,b1,c,b2,m2,a2 iff ( between a1,c,a2 & between b1,c,b2 & c,a1 equiv c,b1 & c,a2 equiv c,b2 & Middle a1,m1,b1 & Middle a2,m2,b2 ) );