theorem ThMak7: :: GTARSKI3:140

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