theorem :: GTARSKI3:139

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