theorem FlatNormal: :: GTARSKI1:34

for S being satisfying_Tarski-model TarskiGeometryStruct
for c, d, e, d9 being POINT of S st between d,e,d9 & c,d9 equiv c,d & d,e equiv d9,e & c <> d & e <> d holds
ex p, r, q being POINT of S st
( between p,r,q & between r,c,d9 & between e,c,p & r,c,p cong r,c,q & r,c equiv e,c & p,r equiv d,e )