theorem ThMak6: :: GTARSKI3:138

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