for S being (RE) (TE) TarskiGeometryStruct holds
( S is satisfying_SAS iff S is (FS) )