for S being non empty (TE) (IE) (SC) (FS') TarskiGeometryStruct holds S is (RE) by ThMak6;