let S be non empty (TE) (IE) (SC) (FS') TarskiGeometryStruct ; :: thesis: S is (FS)
S is (RE) by ThMak6;
hence S is (FS) ; :: thesis: verum