let X be OrtAfPl; :: thesis: ( X is satisfying_PAP iff Af X is Pappian )
A1: ( X is satisfying_PAP implies Af X is Pappian )

proof

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

now

let M, N be Subset of (Af X); :: thesis: for o, a, b, c, a1, b1, c1 being Element of (Af X) st M is being_line & N is being_line & M <> N & o in M & o in N & o <> a & o <> a1 & o <> b & o <> b1 & o <> c & o <> c1 & a in M & b in M & c in M & a1 in N & b1 in N & c1 in N & a,b1 // b,a1 & b,c1 // c,b1 holds
a,c1 // c,a1
let o, a, b, c, a1, b1, c1 be Element of (Af X); :: thesis: ( M is being_line & N is being_line & M <> N & o in M & o in N & o <> a & o <> a1 & o <> b & o <> b1 & o <> c & o <> c1 & a in M & b in M & c in M & a1 in N & b1 in N & c1 in N & a,b1 // b,a1 & b,c1 // c,b1 implies a,c1 // c,a1 )
assume A3: ( M is being_line & N is being_line & M <> N & o in M & o in N & o <> a & o <> a1 & o <> b & o <> b1 & o <> c & o <> c1 & a in M & b in M & c in M & a1 in N & b1 in N & c1 in N & a,b1 // b,a1 & b,c1 // c,b1 ) ; :: thesis: a,c1 // c,a1
reconsider M' = M, N' = N as Subset of X by ANALMETR:57;
reconsider a' = a, b' = b, c' = c, a1' = a1, b1' = b1, c1' = c1 as Element of X by ANALMETR:47;
A4: ( M' is being_line & N' is being_line ) by A3, ANALMETR:58;
b,a1 // a,b1 by A3, AFF_1:13;
then A5: ( b',a1' // a',b1' & b',c1' // c',b1' ) by A3, ANALMETR:48;
( not c1' in M' & not b' in N' )

proof

assume ( c1' in M' or b' in N' ) ; :: thesis: contradiction
then A6: ( o,c1 // M or o,b // N ) by A3, AFF_1:66;
( o,c1 // N & o,b // M ) by A3, AFF_1:66;
then M // N by A3, A6, AFF_1:67;
hence contradiction by A3, AFF_1:59; :: thesis: verum

end;

then a',c1' // c',a1' by A2, A3, A4, A5, CONMETR:def 2;
hence a,c1 // c,a1 by ANALMETR:48; :: thesis: verum

end;

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

end;

( Af X is Pappian implies X is satisfying_PAP )

proof

assume A7: Af X is Pappian ; :: thesis: X is satisfying_PAP

now

let o', a1', a2', a3', b1', b2', b3' be Element of X; :: thesis: for M', N' being Subset of X 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 X; :: 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 A8: ( 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' ) ; :: thesis: a1',b2' // a2',b3'
reconsider M = M', N = N' as Subset of (Af X) by ANALMETR:57;
reconsider a1 = a1', a2 = a2', a3 = a3', b1 = b1', b2 = b2', b3 = b3' as Element of (Af X) by ANALMETR:47;
A9: ( M is being_line & N is being_line ) by A8, ANALMETR:58;

now

assume M <> N ; :: thesis: a1',b2' // a2',b3'
( a3,b2 // a2,b1 & a3,b3 // a1,b1 ) by A8, ANALMETR:48;
then ( a3,b2 // a2,b1 & a1,b1 // a3,b3 ) by AFF_1:13;
then a1,b2 // a2,b3 by A7, A8, A9, AFF_2:def 2;
hence a1',b2' // a2',b3' by ANALMETR:48; :: thesis: verum

end;

hence a1',b2' // a2',b3' by A8; :: thesis: verum

end;

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

end;

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