theorem Th3: :: CONMETR1:3

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