theorem ThMak3: :: GTARSKI3:130

for S being TarskiGeometryStruct st S is (RE) & S is (TE) holds
( S is (FS) iff S is (FS') )