theorem :: CONMETR1:12

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