let AP be AffinPlane; :: thesis: ( AP is satisfying_PPAP iff ( AP is Pappian & AP is satisfying_pap ) )
A1: ( AP is Pappian & AP is satisfying_pap implies AP is satisfying_PPAP )

proof

assume that
A2: AP is Pappian and
A3: AP is satisfying_pap ; :: thesis: AP is satisfying_PPAP
thus AP is satisfying_PPAP :: thesis: verum

proof

let M be Subset of ; :: according to AFF_2:def 1 :: thesis: for N being Subset of
for a, b, c, a', b', c' being Element of st M is being_line & N is being_line & 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 N be Subset of ; :: thesis: for a, b, c, a', b', c' being Element of st M is being_line & N is being_line & 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 a, b, c, a', b', c' be Element of ; :: thesis: ( M is being_line & N is being_line & 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
A4: M is being_line and
A5: N is being_line and
A6: a in M and
A7: b in M and
A8: c in M and
A9: a' in N and
A10: b' in N and
A11: c' in N and
A12: a,b' // b,a' and
A13: b,c' // c,b' ; :: thesis: a,c' // c,a'

now

assume A14: M <> N ; :: thesis: ( not a,c' // c,a' implies a,c' // c,a' )
assume A15: not a,c' // c,a' ; :: thesis: a,c' // c,a'

now

assume not M // N ; :: thesis: a,c' // c,a'
then consider o being Element of such that
A16: o in M and
A17: o in N by A4, A5, AFF_1:72;
A18: o <> a

proof

assume A19: o = a ; :: thesis: contradiction
then o,b' // a',b by A12, AFF_1:13;
then ( o = b' or b in N ) by A5, A9, A10, A17, AFF_1:62;
then ( o = b' or o = b ) by A4, A5, A7, A14, A16, A17, AFF_1:30;
then ( c,o // b,c' or o,c' // b',c ) by A13, AFF_1:13;
then ( c' in M or c = o or c in N or o = c' ) by A4, A5, A7, A8, A10, A11, A16, A17, AFF_1:62;
then ( o = c or o = c' ) by A4, A5, A8, A11, A14, A16, A17, AFF_1:30;
hence contradiction by A5, A9, A11, A15, A17, A19, AFF_1:12, AFF_1:65; :: thesis: verum

end;

A20: o <> b

proof

assume A21: o = b ; :: thesis: contradiction
then o,c' // b',c by A13, AFF_1:13;
then ( o = c' or c in N ) by A5, A10, A11, A17, AFF_1:62;
then A22: ( o = c' or o = c ) by A4, A5, A8, A14, A16, A17, AFF_1:30;
o,a' // b',a by A12, A21, AFF_1:13;
then ( o = a' or a in N ) by A5, A9, A10, A17, AFF_1:62;
hence contradiction by A4, A5, A6, A8, A14, A15, A16, A17, A18, A22, AFF_1:12, AFF_1:30, AFF_1:65; :: thesis: verum

end;

A23: o <> c'

proof

assume A24: o = c' ; :: thesis: contradiction
then b' in M by A4, A7, A8, A13, A16, A20, AFF_1:62;
then a,o // b,a' by A4, A5, A10, A12, A14, A16, A17, AFF_1:30;
then a' in M by A4, A6, A7, A16, A18, AFF_1:62;
hence contradiction by A4, A6, A8, A15, A16, A24, AFF_1:65; :: thesis: verum

end;

A25: o <> c

proof

assume A26: o = c ; :: thesis: contradiction
then o,b' // c',b by A13, AFF_1:13;
then ( o = b' or b in N ) by A5, A10, A11, A17, AFF_1:62;
then a' in M by A4, A5, A6, A7, A9, A12, A16, A17, A18, A20, AFF_1:30, AFF_1:62;
then a' = o by A4, A5, A9, A14, A16, A17, AFF_1:30;
hence contradiction by A15, A26, AFF_1:12; :: thesis: verum

end;

A27: o <> a'

proof

assume A28: o = a' ; :: thesis: contradiction
then o,b // a,b' by A12, AFF_1:13;
then b' in M by A4, A6, A7, A16, A20, AFF_1:62;
then o = b' by A4, A5, A10, A14, A16, A17, AFF_1:30;
then c,o // b,c' by A13, AFF_1:13;
then c' in M by A4, A7, A8, A16, A25, AFF_1:62;
hence contradiction by A4, A6, A8, A15, A16, A28, AFF_1:65; :: thesis: verum

end;

o <> b'

proof

assume A29: o = b' ; :: thesis: contradiction
then o,c // b,c' by A13, AFF_1:13;
then A30: c' in M by A4, A7, A8, A16, A25, AFF_1:62;
a' in M by A4, A6, A7, A12, A16, A18, A29, AFF_1:62;
hence contradiction by A4, A6, A8, A15, A30, AFF_1:65; :: thesis: verum

end;

hence a,c' // c,a' by A2, A4, A5, A6, A7, A8, A9, A10, A11, A12, A13, A14, A16, A17, A18, A20, A25, A27, A23, Def2; :: thesis: verum

end;

hence a,c' // c,a' by A3, A4, A5, A6, A7, A8, A9, A10, A11, A12, A13, A14, Def13; :: thesis: verum

end;

hence a,c' // c,a' by A4, A6, A8, A9, A11, AFF_1:65; :: thesis: verum

end;

end;

( AP is satisfying_PPAP implies ( AP is Pappian & AP is satisfying_pap ) )

proof

assume A31: AP is satisfying_PPAP ; :: thesis: ( AP is Pappian & AP is satisfying_pap )
thus AP is Pappian :: thesis: AP is satisfying_pap

proof

let M be Subset of ; :: according to AFF_2:def 2 :: thesis: for N being Subset of
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 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
A32: ( M is being_line & N is being_line ) and
M <> N and
o in M and
o in N and
o <> a and
o <> a' and
o <> b and
o <> b' and
o <> c and
o <> c' and
A33: ( 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' ) ; :: thesis: a,c' // c,a'
thus a,c' // c,a' by A31, A32, A33, Def1; :: thesis: verum

end;

thus AP is satisfying_pap :: thesis: verum

proof

let M be Subset of ; :: according to AFF_2:def 13 :: thesis: for N being Subset of
for a, b, c, a', b', c' being Element of st M is being_line & N is being_line & a in M & b in M & c in M & M // N & M <> N & a' in N & b' in N & c' in N & a,b' // b,a' & b,c' // c,b' holds
a,c' // c,a'
let N be Subset of ; :: thesis: for a, b, c, a', b', c' being Element of st M is being_line & N is being_line & a in M & b in M & c in M & M // N & M <> N & a' in N & b' in N & c' in N & a,b' // b,a' & b,c' // c,b' holds
a,c' // c,a'
let a, b, c, a', b', c' be Element of ; :: thesis: ( M is being_line & N is being_line & a in M & b in M & c in M & M // N & M <> N & a' in N & b' in N & c' in N & a,b' // b,a' & b,c' // c,b' implies a,c' // c,a' )
assume that
A34: ( M is being_line & N is being_line & a in M & b in M & c in M ) and
M // N and
M <> N and
A35: ( a' in N & b' in N & c' in N & a,b' // b,a' & b,c' // c,b' ) ; :: thesis: a,c' // c,a'
thus a,c' // c,a' by A31, A34, A35, Def1; :: thesis: verum

end;

end;

hence ( AP is satisfying_PPAP iff ( AP is Pappian & AP is satisfying_pap ) ) by A1; :: thesis: verum