:: deftheorem defines satisfying_Tarski-model GTARSKI1:def 12 :
for S being TarskiGeometryStruct holds
( S is satisfying_Tarski-model iff ( S is satisfying_CongruenceSymmetry & S is satisfying_CongruenceEquivalenceRelation & S is satisfying_CongruenceIdentity & S is satisfying_SegmentConstruction & S is satisfying_SAS & S is satisfying_BetweennessIdentity & S is satisfying_Pasch ) );