for X being AffinPlane st X is satisfying_major_indirect_Scherungssatz holds
X is satisfying_major_Scherungssatz