theorem :: GTARSKI3:126

for S being TarskiGeometryStruct holds
( S is satisfying_Euclid_Axiom iff S is (Eu) ) ;