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