theorem :: GTARSKI3:137

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