let S be TarskiGeometryStruct ; :: thesis: ( S is (RE) & S is (TE) implies ( S is (FS) iff S is (FS') ) )
assume that
A1: S is (RE) and
A2: S is (TE) ; :: thesis: ( S is (FS) iff S is (FS') )
hereby :: thesis: ( S is (FS') implies S is (FS) )
assume A3: S is (FS) ; :: thesis: S is (FS')
thus S is (FS') :: thesis: verum
proof
let a, b, c, d, a9, b9, c9, d9 be POINT of S; :: according to GTARSKI3:def 26 :: thesis: ( a <> b & between a,b,c & between a9,b9,c9 & a,b equiv a9,b9 & b,c equiv b9,c9 & a,d equiv a9,d9 & b,d equiv b9,d9 implies d,c equiv c9,d9 )
assume ( a <> b & between a,b,c & between a9,b9,c9 & a,b equiv a9,b9 & b,c equiv b9,c9 & a,d equiv a9,d9 & b,d equiv b9,d9 ) ; :: thesis: d,c equiv c9,d9
then ( c,d equiv c9,d9 & c,d equiv d,c ) by A1, A3;
hence d,c equiv c9,d9 by A2; :: thesis: verum
end;
end;
assume A4: S is (FS') ; :: thesis: S is (FS)
let a, b, c, d, a9, b9, c9, d9 be POINT of S; :: according to GTARSKI3:def 19 :: thesis: ( a <> b & between a,b,c & between a9,b9,c9 & a,b equiv a9,b9 & b,c equiv b9,c9 & a,d equiv a9,d9 & b,d equiv b9,d9 implies c,d equiv c9,d9 )
assume ( a <> b & between a,b,c & between a9,b9,c9 & a,b equiv a9,b9 & b,c equiv b9,c9 & a,d equiv a9,d9 & b,d equiv b9,d9 ) ; :: thesis: c,d equiv c9,d9
then ( d,c equiv c9,d9 & d,c equiv c,d ) by A1, A4;
hence c,d equiv c9,d9 by A2; :: thesis: verum