theorem ThMak5: :: GTARSKI3:136

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