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 )

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

proof

thus
( AP is satisfying_PPAP iff ( AP is Pappian & AP is satisfying_pap ) )
by A1; :: thesis: verum
assume that

A2: AP is Pappian and

A3: AP is satisfying_pap ; :: thesis: AP is satisfying_PPAP

thus AP is satisfying_PPAP :: thesis: verum

end;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 AP; :: according to AFF_2:def 1 :: thesis: for 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

let N be Subset of AP; :: thesis: 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

let a, b, c, a9, b9, c9 be Element of AP; :: thesis: ( 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 implies a,c9 // c,a9 )

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: a9 in N and

A10: b9 in N and

A11: c9 in N and

A12: a,b9 // b,a9 and

A13: b,c9 // c,b9 ; :: thesis: a,c9 // c,a9

end;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

let N be Subset of AP; :: thesis: 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

let a, b, c, a9, b9, c9 be Element of AP; :: thesis: ( 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 implies a,c9 // c,a9 )

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: a9 in N and

A10: b9 in N and

A11: c9 in N and

A12: a,b9 // b,a9 and

A13: b,c9 // c,b9 ; :: thesis: a,c9 // c,a9

now :: thesis: ( M <> N & not a,c9 // c,a9 implies a,c9 // c,a9 )

hence
a,c9 // c,a9
by A4, A6, A8, A9, A11, AFF_1:51; :: thesis: verumassume A14:
M <> N
; :: thesis: ( not a,c9 // c,a9 implies a,c9 // c,a9 )

assume A15: not a,c9 // c,a9 ; :: thesis: a,c9 // c,a9

end;assume A15: not a,c9 // c,a9 ; :: thesis: a,c9 // c,a9

now :: thesis: ( not M // N implies a,c9 // c,a9 )

hence
a,c9 // c,a9
by A3, A4, A5, A6, A7, A8, A9, A10, A11, A12, A13, A14; :: thesis: verumassume
not M // N
; :: thesis: a,c9 // c,a9

then consider o being Element of AP such that

A16: o in M and

A17: o in N by A4, A5, AFF_1:58;

A18: o <> a

end;then consider o being Element of AP such that

A16: o in M and

A17: o in N by A4, A5, AFF_1:58;

A18: o <> a

proof

A20:
o <> b
assume A19:
o = a
; :: thesis: contradiction

then o,b9 // a9,b by A12, AFF_1:4;

then ( o = b9 or b in N ) by A5, A9, A10, A17, AFF_1:48;

then ( o = b9 or o = b ) by A4, A5, A7, A14, A16, A17, AFF_1:18;

then ( c,o // b,c9 or o,c9 // b9,c ) by A13, AFF_1:4;

then ( c9 in M or c = o or c in N or o = c9 ) by A4, A5, A7, A8, A10, A11, A16, A17, AFF_1:48;

then ( o = c or o = c9 ) by A4, A5, A8, A11, A14, A16, A17, AFF_1:18;

hence contradiction by A5, A9, A11, A15, A17, A19, AFF_1:3, AFF_1:51; :: thesis: verum

end;then o,b9 // a9,b by A12, AFF_1:4;

then ( o = b9 or b in N ) by A5, A9, A10, A17, AFF_1:48;

then ( o = b9 or o = b ) by A4, A5, A7, A14, A16, A17, AFF_1:18;

then ( c,o // b,c9 or o,c9 // b9,c ) by A13, AFF_1:4;

then ( c9 in M or c = o or c in N or o = c9 ) by A4, A5, A7, A8, A10, A11, A16, A17, AFF_1:48;

then ( o = c or o = c9 ) by A4, A5, A8, A11, A14, A16, A17, AFF_1:18;

hence contradiction by A5, A9, A11, A15, A17, A19, AFF_1:3, AFF_1:51; :: thesis: verum

proof

A23:
o <> c9
assume A21:
o = b
; :: thesis: contradiction

then o,c9 // b9,c by A13, AFF_1:4;

then ( o = c9 or c in N ) by A5, A10, A11, A17, AFF_1:48;

then A22: ( o = c9 or o = c ) by A4, A5, A8, A14, A16, A17, AFF_1:18;

o,a9 // b9,a by A12, A21, AFF_1:4;

then ( o = a9 or a in N ) by A5, A9, A10, A17, AFF_1:48;

hence contradiction by A4, A5, A6, A8, A14, A15, A16, A17, A18, A22, AFF_1:3, AFF_1:18, AFF_1:51; :: thesis: verum

end;then o,c9 // b9,c by A13, AFF_1:4;

then ( o = c9 or c in N ) by A5, A10, A11, A17, AFF_1:48;

then A22: ( o = c9 or o = c ) by A4, A5, A8, A14, A16, A17, AFF_1:18;

o,a9 // b9,a by A12, A21, AFF_1:4;

then ( o = a9 or a in N ) by A5, A9, A10, A17, AFF_1:48;

hence contradiction by A4, A5, A6, A8, A14, A15, A16, A17, A18, A22, AFF_1:3, AFF_1:18, AFF_1:51; :: thesis: verum

proof

A25:
o <> c
assume A24:
o = c9
; :: thesis: contradiction

then b9 in M by A4, A7, A8, A13, A16, A20, AFF_1:48;

then a,o // b,a9 by A4, A5, A10, A12, A14, A16, A17, AFF_1:18;

then a9 in M by A4, A6, A7, A16, A18, AFF_1:48;

hence contradiction by A4, A6, A8, A15, A16, A24, AFF_1:51; :: thesis: verum

end;then b9 in M by A4, A7, A8, A13, A16, A20, AFF_1:48;

then a,o // b,a9 by A4, A5, A10, A12, A14, A16, A17, AFF_1:18;

then a9 in M by A4, A6, A7, A16, A18, AFF_1:48;

hence contradiction by A4, A6, A8, A15, A16, A24, AFF_1:51; :: thesis: verum

proof

A27:
o <> a9
assume A26:
o = c
; :: thesis: contradiction

then o,b9 // c9,b by A13, AFF_1:4;

then ( o = b9 or b in N ) by A5, A10, A11, A17, AFF_1:48;

then a9 in M by A4, A5, A6, A7, A9, A12, A16, A17, A18, A20, AFF_1:18, AFF_1:48;

then a9 = o by A4, A5, A9, A14, A16, A17, AFF_1:18;

hence contradiction by A15, A26, AFF_1:3; :: thesis: verum

end;then o,b9 // c9,b by A13, AFF_1:4;

then ( o = b9 or b in N ) by A5, A10, A11, A17, AFF_1:48;

then a9 in M by A4, A5, A6, A7, A9, A12, A16, A17, A18, A20, AFF_1:18, AFF_1:48;

then a9 = o by A4, A5, A9, A14, A16, A17, AFF_1:18;

hence contradiction by A15, A26, AFF_1:3; :: thesis: verum

proof

o <> b9
assume A28:
o = a9
; :: thesis: contradiction

then o,b // a,b9 by A12, AFF_1:4;

then b9 in M by A4, A6, A7, A16, A20, AFF_1:48;

then o = b9 by A4, A5, A10, A14, A16, A17, AFF_1:18;

then c,o // b,c9 by A13, AFF_1:4;

then c9 in M by A4, A7, A8, A16, A25, AFF_1:48;

hence contradiction by A4, A6, A8, A15, A16, A28, AFF_1:51; :: thesis: verum

end;then o,b // a,b9 by A12, AFF_1:4;

then b9 in M by A4, A6, A7, A16, A20, AFF_1:48;

then o = b9 by A4, A5, A10, A14, A16, A17, AFF_1:18;

then c,o // b,c9 by A13, AFF_1:4;

then c9 in M by A4, A7, A8, A16, A25, AFF_1:48;

hence contradiction by A4, A6, A8, A15, A16, A28, AFF_1:51; :: thesis: verum

proof

hence
a,c9 // c,a9
by A2, A4, A5, A6, A7, A8, A9, A10, A11, A12, A13, A14, A16, A17, A18, A20, A25, A27, A23; :: thesis: verum
assume A29:
o = b9
; :: thesis: contradiction

then o,c // b,c9 by A13, AFF_1:4;

then A30: c9 in M by A4, A7, A8, A16, A25, AFF_1:48;

a9 in M by A4, A6, A7, A12, A16, A18, A29, AFF_1:48;

hence contradiction by A4, A6, A8, A15, A30, AFF_1:51; :: thesis: verum

end;then o,c // b,c9 by A13, AFF_1:4;

then A30: c9 in M by A4, A7, A8, A16, A25, AFF_1:48;

a9 in M by A4, A6, A7, A12, A16, A18, A29, AFF_1:48;

hence contradiction by A4, A6, A8, A15, A30, AFF_1:51; :: thesis: verum