for S being (RE) (TE) TarskiGeometryStruct holds
( S is (FS) iff S is (FS') ) by ThMak3;