let S be (TE) (SC) (FS') TarskiGeometryStruct ; :: thesis: S is (RE')
let a, b, c, d be POINT of S; :: according to GTARSKI3:def 27 :: thesis: ( a <> b & between b,a,c implies d,c equiv c,d )
assume A1: ( a <> b & between b,a,c ) ; :: thesis: d,c equiv c,d
( a,c equiv a,c & b,a equiv b,a & b,d equiv b,d ) by Satz2p1bis;
hence d,c equiv c,d by A1, ThMak4; :: thesis: verum