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