let MS be OrtAfPl; :: thesis: ( MS is satisfying_PAP iff Af MS is Pappian )
set AS = Af MS;

A1: now

assume A2: MS is satisfying_PAP ; :: thesis: Af MS is Pappian

now

let M, N be Subset of ; :: thesis: for o, a, b, c, a', b', c' being Element of st M is being_line & N is being_line & M <> N & o in M & o in N & o <> a & o <> a' & o <> b & o <> b' & o <> c & o <> c' & a in M & b in M & c in M & a' in N & b' in N & c' in N & a,b' // b,a' & b,c' // c,b' holds
a,c' // c,a'
let o, a, b, c, a', b', c' be Element of ; :: thesis: ( M is being_line & N is being_line & M <> N & o in M & o in N & o <> a & o <> a' & o <> b & o <> b' & o <> c & o <> c' & a in M & b in M & c in M & a' in N & b' in N & c' in N & a,b' // b,a' & b,c' // c,b' implies a,c' // c,a' )
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 <> a' & o <> b ) and
A8: ( o <> b' & o <> c & o <> c' & a in M ) and
A9: b in M and
A10: c in M and
A11: a' in N and
A12: ( b' in N & c' in N ) and
A13: a,b' // b,a' and
A14: b,c' // c,b' ; :: thesis: a,c' // c,a'
reconsider M' = M, N' = N as Subset of by ANALMETR:57;
reconsider a1 = a, b1 = b, c1 = c, a1' = a', b1' = b', c1' = c' as Element of by ANALMETR:47;
A15: b1,c1' // c1,b1' by A14, ANALMETR:48;
a1,b1' // b1,a1' by A13, ANALMETR:48;
then A16: b1,a1' // a1,b1' by ANALMETR:81;
A17: ( M' is being_line & N' is being_line ) by A3, ANALMETR:58;
then ( not a1' in M' & not b1 in N' ) by A4, A5, A7, A9, A11, CONMETR:5;
then c1,a1' // a1,c1' by A2, A5, A6, A8, A9, A10, A11, A12, A17, A16, A15, CONMETR:def 2;
then a1,c1' // c1,a1' by ANALMETR:81;
hence a,c' // c,a' by ANALMETR:48; :: thesis: verum

end;

hence Af MS is Pappian by AFF_2:def 2; :: thesis: verum

end;

now

assume A18: Af MS is Pappian ; :: thesis: MS is satisfying_PAP

now

let o, a1, a2, a3, b1, b2, b3 be Element of ; :: thesis: for M, N being Subset of 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 ; :: 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 M' = M, N' = N as Subset of by ANALMETR:57;
reconsider a = a1, b = a2, c = a3, a' = b1, b' = b2, c' = b3 as Element of by ANALMETR:47;
A25: c,c' // a,a' by A24, ANALMETR:48;
a2,b1 // a3,b2 by A23, ANALMETR:81;
then A26: b,a' // c,b' by ANALMETR:48;
( M' is being_line & N' is being_line ) by A19, ANALMETR:58;
then b,c' // a,b' by A18, A20, A21, A22, A26, A25, AFF_2:def 2;
then a2,b3 // a1,b2 by ANALMETR:48;
hence a1,b2 // a2,b3 by ANALMETR:81; :: thesis: verum

end;

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

end;

hence ( MS is satisfying_PAP iff Af MS is Pappian ) by A1; :: thesis: verum