for S being (TE) (SC) (FS') TarskiGeometryStruct holds S is (RE')