let X be AffinPlane; :: thesis: ( X is satisfying_indirect_Scherungssatz implies X is satisfying_Scherungssatz )
assume X is satisfying_indirect_Scherungssatz ; :: thesis: X is satisfying_Scherungssatz
then ( X is satisfying_minor_indirect_Scherungssatz & X is satisfying_major_indirect_Scherungssatz ) by Th1;
then ( X is satisfying_minor_Scherungssatz & X is satisfying_major_Scherungssatz ) by Th3, Th4;
hence X is satisfying_Scherungssatz by Th2; :: thesis: verum