for S being non empty (TE) (IE) (SC) (FS') TarskiGeometryStruct holds S is (FS)