for X being AffinPlane holds
( X is Desarguesian iff X is satisfying_Scherungssatz )