theorem ThMak2: :: GTARSKI3:129
for S being (RE) (TE) TarskiGeometryStruct holds
( S is satisfying_SAS iff S is (FS) )