let S be (TE) (SC) (FS') TarskiGeometryStruct ; :: thesis: for a, b, c, d, e, f being POINT of S st a <> b & between b,a,c & between d,a,e & b,a equiv d,a & a,c equiv a,e & b,f equiv d,f holds
f,c equiv e,f
let a, b, c, d, e, f be POINT of S; :: thesis: ( a <> b & between b,a,c & between d,a,e & b,a equiv d,a & a,c equiv a,e & b,f equiv d,f implies f,c equiv e,f )
assume A1: ( a <> b & between b,a,c & between d,a,e & b,a equiv d,a & a,c equiv a,e & b,f equiv d,f ) ; :: thesis: f,c equiv e,f
A2: a,f equiv a,f by Satz2p1bis;
S is (FS') ;
hence f,c equiv e,f by A1, A2; :: thesis: verum