:: deftheorem defines satisfying_PPAP AFF_2:def 1 :
for AP being AffinPlane holds
( AP is satisfying_PPAP iff for M, N being Subset of AP
for a, b, c, a9, b9, c9 being Element of AP st M is being_line & N is being_line & a in M & b in M & c in M & a9 in N & b9 in N & c9 in N & a,b9 // b,a9 & b,c9 // c,b9 holds
a,c9 // c,a9 );