theorem :: GTARSKI3:123

for S being TarskiGeometryStruct holds
( S is satisfying_Pasch iff S is (Pa) ) ;