let AP be AffinPlane; :: thesis: ( AP is Pappian iff AP is satisfying_PAP_1 )

let M be Subset of AP; :: according to AFF_2:def 2 :: thesis: for N being Subset of AP

for o, a, b, c, a9, b9, c9 being Element of AP 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 N be Subset of AP; :: thesis: for o, a, b, c, a9, b9, c9 being Element of AP 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 AP; :: 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

A32: M is being_line and

A33: N is being_line and

A34: ( M <> N & o in M & o in N ) and

A35: o <> a and

A36: o <> a9 and

A37: o <> b and

A38: o <> b9 and

A39: ( o <> c & o <> c9 ) and

A40: a in M and

A41: b in M and

A42: c in M and

A43: a9 in N and

A44: b9 in N and

A45: c9 in N and

A46: a,b9 // b,a9 and

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

set A = Line (a,c9);

set P = Line (b,a9);

A48: b <> a9 by A32, A33, A34, A36, A41, A43, AFF_1:18;

then A49: b in Line (b,a9) by AFF_1:24;

assume A50: not a,c9 // c,a9 ; :: thesis: contradiction

then A51: a <> c9 by AFF_1:3;

then A52: ( a in Line (a,c9) & c9 in Line (a,c9) ) by AFF_1:24;

A53: a9 in Line (b,a9) by A48, AFF_1:24;

Line (a,c9) is being_line by A51, AFF_1:24;

then consider K being Subset of AP such that

A54: c in K and

A55: Line (a,c9) // K by AFF_1:49;

A56: b <> c

K is being_line by A55, AFF_1:36;

then consider x being Element of AP such that

A61: x in Line (b,a9) and

A62: x in K by A60, A59, AFF_1:58;

A63: a,c9 // c,x by A52, A54, A55, A62, AFF_1:39;

LIN b,x,a9 by A60, A49, A53, A61, AFF_1:21;

then b,x // b,a9 by AFF_1:def 1;

then a,b9 // b,x by A46, A48, AFF_1:5;

then x in N by A31, A32, A33, A34, A35, A37, A38, A39, A40, A41, A42, A44, A45, A47, A56, A63;

then N = Line (b,a9) by A33, A43, A50, A60, A53, A61, A63, AFF_1:18;

hence contradiction by A32, A33, A34, A37, A41, A49, AFF_1:18; :: thesis: verum

hereby :: thesis: ( AP is satisfying_PAP_1 implies AP is Pappian )

assume A31:
AP is satisfying_PAP_1
; :: thesis: AP is Pappian assume A1:
AP is Pappian
; :: thesis: AP is satisfying_PAP_1

thus AP is satisfying_PAP_1 :: thesis: verum

end;thus AP is satisfying_PAP_1 :: thesis: verum

proof

let M be Subset of AP; :: according to AFF_2:def 3 :: thesis: for N being Subset of AP

for o, a, b, c, a9, b9, c9 being Element of AP 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 & b9 in N & c9 in N & a,b9 // b,a9 & b,c9 // c,b9 & a,c9 // c,a9 & b <> c holds

a9 in N

let N be Subset of AP; :: thesis: for o, a, b, c, a9, b9, c9 being Element of AP 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 & b9 in N & c9 in N & a,b9 // b,a9 & b,c9 // c,b9 & a,c9 // c,a9 & b <> c holds

a9 in N

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

assume that

A2: M is being_line and

A3: N is being_line and

A4: M <> N and

A5: o in M and

A6: o in N and

A7: o <> a and

o <> a9 and

A8: o <> b and

A9: o <> b9 and

A10: o <> c and

A11: o <> c9 and

A12: a in M and

A13: b in M and

A14: c in M and

A15: b9 in N and

A16: c9 in N and

A17: a,b9 // b,a9 and

A18: b,c9 // c,b9 and

A19: a,c9 // c,a9 and

A20: b <> c ; :: thesis: a9 in N

A21: a <> c9 by A2, A3, A4, A5, A6, A7, A12, A16, AFF_1:18;

A22: b <> a9

A24: x in N and

A25: LIN b,a9,x by A3, AFF_1:59;

A26: b,a9 // b,x by A25, AFF_1:def 1;

A27: o <> x

then a,c9 // c,x by A1, A2, A3, A4, A5, A6, A7, A8, A9, A10, A11, A12, A13, A14, A15, A16, A18, A24, A27;

then c,a9 // c,x by A19, A21, AFF_1:5;

then LIN c,a9,x by AFF_1:def 1;

then A28: LIN a9,x,c by AFF_1:6;

A29: LIN a9,x,x by AFF_1:7;

assume A30: not a9 in N ; :: thesis: contradiction

LIN a9,x,b by A25, AFF_1:6;

then x in M by A2, A13, A14, A20, A30, A24, A28, A29, AFF_1:8, AFF_1:25;

hence contradiction by A2, A3, A4, A5, A6, A24, A27, AFF_1:18; :: thesis: verum

end;for o, a, b, c, a9, b9, c9 being Element of AP 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 & b9 in N & c9 in N & a,b9 // b,a9 & b,c9 // c,b9 & a,c9 // c,a9 & b <> c holds

a9 in N

let N be Subset of AP; :: thesis: for o, a, b, c, a9, b9, c9 being Element of AP 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 & b9 in N & c9 in N & a,b9 // b,a9 & b,c9 // c,b9 & a,c9 // c,a9 & b <> c holds

a9 in N

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

assume that

A2: M is being_line and

A3: N is being_line and

A4: M <> N and

A5: o in M and

A6: o in N and

A7: o <> a and

o <> a9 and

A8: o <> b and

A9: o <> b9 and

A10: o <> c and

A11: o <> c9 and

A12: a in M and

A13: b in M and

A14: c in M and

A15: b9 in N and

A16: c9 in N and

A17: a,b9 // b,a9 and

A18: b,c9 // c,b9 and

A19: a,c9 // c,a9 and

A20: b <> c ; :: thesis: a9 in N

A21: a <> c9 by A2, A3, A4, A5, A6, A7, A12, A16, AFF_1:18;

A22: b <> a9

proof

not b,a9 // N
assume
b = a9
; :: thesis: contradiction

then c,b // a,c9 by A19, AFF_1:4;

then c9 in M by A2, A12, A13, A14, A20, AFF_1:48;

hence contradiction by A2, A3, A4, A5, A6, A11, A16, AFF_1:18; :: thesis: verum

end;then c,b // a,c9 by A19, AFF_1:4;

then c9 in M by A2, A12, A13, A14, A20, AFF_1:48;

hence contradiction by A2, A3, A4, A5, A6, A11, A16, AFF_1:18; :: thesis: verum

proof

then consider x being Element of AP such that
assume A23:
b,a9 // N
; :: thesis: contradiction

b,a9 // a,b9 by A17, AFF_1:4;

then a,b9 // N by A22, A23, AFF_1:32;

then b9,a // N by AFF_1:34;

then a in N by A3, A15, AFF_1:23;

hence contradiction by A2, A3, A4, A5, A6, A7, A12, AFF_1:18; :: thesis: verum

end;b,a9 // a,b9 by A17, AFF_1:4;

then a,b9 // N by A22, A23, AFF_1:32;

then b9,a // N by AFF_1:34;

then a in N by A3, A15, AFF_1:23;

hence contradiction by A2, A3, A4, A5, A6, A7, A12, AFF_1:18; :: thesis: verum

A24: x in N and

A25: LIN b,a9,x by A3, AFF_1:59;

A26: b,a9 // b,x by A25, AFF_1:def 1;

A27: o <> x

proof

a,b9 // b,x
by A17, A22, A26, AFF_1:5;
assume
o = x
; :: thesis: contradiction

then b,o // a,b9 by A17, A22, A26, AFF_1:5;

then b9 in M by A2, A5, A8, A12, A13, AFF_1:48;

hence contradiction by A2, A3, A4, A5, A6, A9, A15, AFF_1:18; :: thesis: verum

end;then b,o // a,b9 by A17, A22, A26, AFF_1:5;

then b9 in M by A2, A5, A8, A12, A13, AFF_1:48;

hence contradiction by A2, A3, A4, A5, A6, A9, A15, AFF_1:18; :: thesis: verum

then a,c9 // c,x by A1, A2, A3, A4, A5, A6, A7, A8, A9, A10, A11, A12, A13, A14, A15, A16, A18, A24, A27;

then c,a9 // c,x by A19, A21, AFF_1:5;

then LIN c,a9,x by AFF_1:def 1;

then A28: LIN a9,x,c by AFF_1:6;

A29: LIN a9,x,x by AFF_1:7;

assume A30: not a9 in N ; :: thesis: contradiction

LIN a9,x,b by A25, AFF_1:6;

then x in M by A2, A13, A14, A20, A30, A24, A28, A29, AFF_1:8, AFF_1:25;

hence contradiction by A2, A3, A4, A5, A6, A24, A27, AFF_1:18; :: thesis: verum

let M be Subset of AP; :: according to AFF_2:def 2 :: thesis: for N being Subset of AP

for o, a, b, c, a9, b9, c9 being Element of AP 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 N be Subset of AP; :: thesis: for o, a, b, c, a9, b9, c9 being Element of AP 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 AP; :: 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

A32: M is being_line and

A33: N is being_line and

A34: ( M <> N & o in M & o in N ) and

A35: o <> a and

A36: o <> a9 and

A37: o <> b and

A38: o <> b9 and

A39: ( o <> c & o <> c9 ) and

A40: a in M and

A41: b in M and

A42: c in M and

A43: a9 in N and

A44: b9 in N and

A45: c9 in N and

A46: a,b9 // b,a9 and

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

set A = Line (a,c9);

set P = Line (b,a9);

A48: b <> a9 by A32, A33, A34, A36, A41, A43, AFF_1:18;

then A49: b in Line (b,a9) by AFF_1:24;

assume A50: not a,c9 // c,a9 ; :: thesis: contradiction

then A51: a <> c9 by AFF_1:3;

then A52: ( a in Line (a,c9) & c9 in Line (a,c9) ) by AFF_1:24;

A53: a9 in Line (b,a9) by A48, AFF_1:24;

Line (a,c9) is being_line by A51, AFF_1:24;

then consider K being Subset of AP such that

A54: c in K and

A55: Line (a,c9) // K by AFF_1:49;

A56: b <> c

proof

A58:
b9 <> c9
assume A57:
b = c
; :: thesis: contradiction

then LIN b,c9,b9 by A47, AFF_1:def 1;

then LIN b9,c9,b by AFF_1:6;

then ( b9 = c9 or b in N ) by A33, A44, A45, AFF_1:25;

hence contradiction by A32, A33, A34, A37, A41, A46, A50, A57, AFF_1:18; :: thesis: verum

end;then LIN b,c9,b9 by A47, AFF_1:def 1;

then LIN b9,c9,b by AFF_1:6;

then ( b9 = c9 or b in N ) by A33, A44, A45, AFF_1:25;

hence contradiction by A32, A33, A34, A37, A41, A46, A50, A57, AFF_1:18; :: thesis: verum

proof

A59:
not Line (b,a9) // K
assume
b9 = c9
; :: thesis: contradiction

then b9,b // b9,c by A47, AFF_1:4;

then LIN b9,b,c by AFF_1:def 1;

then LIN b,c,b9 by AFF_1:6;

then b9 in M by A32, A41, A42, A56, AFF_1:25;

hence contradiction by A32, A33, A34, A38, A44, AFF_1:18; :: thesis: verum

end;then b9,b // b9,c by A47, AFF_1:4;

then LIN b9,b,c by AFF_1:def 1;

then LIN b,c,b9 by AFF_1:6;

then b9 in M by A32, A41, A42, A56, AFF_1:25;

hence contradiction by A32, A33, A34, A38, A44, AFF_1:18; :: thesis: verum

proof

A60:
Line (b,a9) is being_line
by A48, AFF_1:24;
assume
Line (b,a9) // K
; :: thesis: contradiction

then Line (b,a9) // Line (a,c9) by A55, AFF_1:44;

then b,a9 // a,c9 by A52, A49, A53, AFF_1:39;

then a,b9 // a,c9 by A46, A48, AFF_1:5;

then LIN a,b9,c9 by AFF_1:def 1;

then LIN b9,c9,a by AFF_1:6;

then a in N by A33, A44, A45, A58, AFF_1:25;

hence contradiction by A32, A33, A34, A35, A40, AFF_1:18; :: thesis: verum

end;then Line (b,a9) // Line (a,c9) by A55, AFF_1:44;

then b,a9 // a,c9 by A52, A49, A53, AFF_1:39;

then a,b9 // a,c9 by A46, A48, AFF_1:5;

then LIN a,b9,c9 by AFF_1:def 1;

then LIN b9,c9,a by AFF_1:6;

then a in N by A33, A44, A45, A58, AFF_1:25;

hence contradiction by A32, A33, A34, A35, A40, AFF_1:18; :: thesis: verum

K is being_line by A55, AFF_1:36;

then consider x being Element of AP such that

A61: x in Line (b,a9) and

A62: x in K by A60, A59, AFF_1:58;

A63: a,c9 // c,x by A52, A54, A55, A62, AFF_1:39;

LIN b,x,a9 by A60, A49, A53, A61, AFF_1:21;

then b,x // b,a9 by AFF_1:def 1;

then a,b9 // b,x by A46, A48, AFF_1:5;

then x in N by A31, A32, A33, A34, A35, A37, A38, A39, A40, A41, A42, A44, A45, A47, A56, A63;

then N = Line (b,a9) by A33, A43, A50, A60, A53, A61, A63, AFF_1:18;

hence contradiction by A32, A33, A34, A37, A41, A49, AFF_1:18; :: thesis: verum