let X be AffinPlane; :: thesis: ( X is satisfying_major_indirect_Scherungssatz implies X is satisfying_minor_indirect_Scherungssatz )
assume X is satisfying_major_indirect_Scherungssatz ; :: thesis: X is satisfying_minor_indirect_Scherungssatz
then X is Pappian by Th10;
then X is satisfying_pap by AFF_2:9;
hence X is satisfying_minor_indirect_Scherungssatz by Th9; :: thesis: verum