theorem Th4: :: CONMETR1:4

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