let X be AffinPlane; :: thesis: ( X is satisfying_PPAP iff X is satisfying_indirect_Scherungssatz )
A1: ( X is satisfying_PPAP implies X is satisfying_indirect_Scherungssatz )

proof

assume A2: X is satisfying_PPAP ; :: thesis: X is satisfying_indirect_Scherungssatz
then X is satisfying_pap by AFF_2:10;
then A3: X is satisfying_minor_indirect_Scherungssatz by Th9;
X is Pappian by A2, AFF_2:10;
then X is satisfying_major_indirect_Scherungssatz by Th10;
hence X is satisfying_indirect_Scherungssatz by A3, Th1; :: thesis: verum

end;

( X is satisfying_indirect_Scherungssatz implies X is satisfying_PPAP )

proof

assume A4: X is satisfying_indirect_Scherungssatz ; :: thesis: X is satisfying_PPAP
then X is satisfying_major_indirect_Scherungssatz ;
then A5: X is Pappian by Th10;
X is satisfying_minor_indirect_Scherungssatz by A4, Th1;
then X is satisfying_pap by Th9;
hence X is satisfying_PPAP by A5, AFF_2:10; :: thesis: verum

end;

hence ( X is satisfying_PPAP iff X is satisfying_indirect_Scherungssatz ) by A1; :: thesis: verum