let MS be OrtAfPl; :: thesis: ( MS is satisfying_PAP iff AffinStruct(# the carrier of MS, the CONGR of MS #) is Pappian )
set AS = AffinStruct(# the carrier of MS, the CONGR of MS #);

A1: now :: thesis: ( MS is satisfying_PAP implies AffinStruct(# the carrier of MS, the CONGR of MS #) is Pappian )

assume A2: MS is satisfying_PAP ; :: thesis: AffinStruct(# the carrier of MS, the CONGR of MS #) is Pappian

now :: thesis: for M, N being Subset of AffinStruct(# the carrier of MS, the CONGR of MS #)
for o, a, b, c, a9, b9, c9 being Element of AffinStruct(# the carrier of MS, the CONGR of MS #) st M is being_line & N is being_line & M <> N & o in M & o in N & o <> a & o <> a9 & o <> b & o <> b9 & o <> c & o <> c9 & 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

let M, N be Subset of AffinStruct(# the carrier of MS, the CONGR of MS #); :: thesis: for o, a, b, c, a9, b9, c9 being Element of AffinStruct(# the carrier of MS, the CONGR of MS #) st M is being_line & N is being_line & M <> N & o in M & o in N & o <> a & o <> a9 & o <> b & o <> b9 & o <> c & o <> c9 & 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
let o, a, b, c, a9, b9, c9 be Element of AffinStruct(# the carrier of MS, the CONGR of MS #); :: thesis: ( M is being_line & N is being_line & M <> N & o in M & o in N & o <> a & o <> a9 & o <> b & o <> b9 & o <> c & o <> c9 & 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 implies a,c9 // c,a9 )
assume that
A3: ( M is being_line & N is being_line ) and
A4: M <> N and
A5: ( o in M & o in N ) and
A6: o <> a and
A7: ( o <> a9 & o <> b ) and
A8: ( o <> b9 & o <> c & o <> c9 & a in M ) and
A9: b in M and
A10: c in M and
A11: a9 in N and
A12: ( b9 in N & c9 in N ) and
A13: a,b9 // b,a9 and
A14: b,c9 // c,b9 ; :: thesis: a,c9 // c,a9
reconsider M9 = M, N9 = N as Subset of MS ;
reconsider a1 = a, b1 = b, c1 = c, a19 = a9, b19 = b9, c19 = c9 as Element of MS ;
A15: b1,c19 // c1,b19 by A14, ANALMETR:36;
a1,b19 // b1,a19 by A13, ANALMETR:36;
then A16: b1,a19 // a1,b19 by ANALMETR:59;
A17: ( M9 is being_line & N9 is being_line ) by A3, ANALMETR:43;
then ( not a19 in M9 & not b1 in N9 ) by A4, A5, A7, A9, A11, CONMETR:5;
then c1,a19 // a1,c19 by A2, A5, A6, A8, A9, A10, A11, A12, A17, A16, A15, CONMETR:def 2;
then a1,c19 // c1,a19 by ANALMETR:59;
hence a,c9 // c,a9 by ANALMETR:36; :: thesis: verum

end;

hence AffinStruct(# the carrier of MS, the CONGR of MS #) is Pappian by AFF_2:def 2; :: thesis: verum

end;

now :: thesis: ( AffinStruct(# the carrier of MS, the CONGR of MS #) is Pappian implies MS is satisfying_PAP )

assume A18: AffinStruct(# the carrier of MS, the CONGR of MS #) is Pappian ; :: thesis: MS is satisfying_PAP

now :: thesis: for o, a1, a2, a3, b1, b2, b3 being Element of MS
for M, N being Subset of the carrier of MS st M is being_line & N is being_line & o in M & a1 in M & a2 in M & a3 in M & o in N & b1 in N & b2 in N & b3 in N & not b2 in M & not a3 in N & o <> a1 & o <> a2 & o <> a3 & o <> b1 & o <> b2 & o <> b3 & a3,b2 // a2,b1 & a3,b3 // a1,b1 holds
a1,b2 // a2,b3

let o, a1, a2, a3, b1, b2, b3 be Element of MS; :: thesis: for M, N being Subset of the carrier of MS st M is being_line & N is being_line & o in M & a1 in M & a2 in M & a3 in M & o in N & b1 in N & b2 in N & b3 in N & not b2 in M & not a3 in N & o <> a1 & o <> a2 & o <> a3 & o <> b1 & o <> b2 & o <> b3 & a3,b2 // a2,b1 & a3,b3 // a1,b1 holds
a1,b2 // a2,b3
let M, N be Subset of the carrier of MS; :: thesis: ( M is being_line & N is being_line & o in M & a1 in M & a2 in M & a3 in M & o in N & b1 in N & b2 in N & b3 in N & not b2 in M & not a3 in N & o <> a1 & o <> a2 & o <> a3 & o <> b1 & o <> b2 & o <> b3 & a3,b2 // a2,b1 & a3,b3 // a1,b1 implies a1,b2 // a2,b3 )
assume that
A19: ( M is being_line & N is being_line ) and
A20: ( o in M & a1 in M & a2 in M & a3 in M & o in N & b1 in N & b2 in N & b3 in N & not b2 in M & not a3 in N & o <> a1 & o <> a2 ) and
o <> a3 and
A21: o <> b1 and
o <> b2 and
A22: o <> b3 and
A23: a3,b2 // a2,b1 and
A24: a3,b3 // a1,b1 ; :: thesis: a1,b2 // a2,b3
reconsider M9 = M, N9 = N as Subset of AffinStruct(# the carrier of MS, the CONGR of MS #) ;
reconsider a = a1, b = a2, c = a3, a9 = b1, b9 = b2, c9 = b3 as Element of AffinStruct(# the carrier of MS, the CONGR of MS #) ;
A25: c,c9 // a,a9 by A24, ANALMETR:36;
a2,b1 // a3,b2 by A23, ANALMETR:59;
then A26: b,a9 // c,b9 by ANALMETR:36;
( M9 is being_line & N9 is being_line ) by A19, ANALMETR:43;
then b,c9 // a,b9 by A18, A20, A21, A22, A26, A25, AFF_2:def 2;
then a2,b3 // a1,b2 by ANALMETR:36;
hence a1,b2 // a2,b3 by ANALMETR:59; :: thesis: verum

end;

hence MS is satisfying_PAP by CONMETR:def 2; :: thesis: verum

end;

hence ( MS is satisfying_PAP iff AffinStruct(# the carrier of MS, the CONGR of MS #) is Pappian ) by A1; :: thesis: verum