let AP be AffinPlane; :: thesis: ( AP is Pappian implies AP is satisfying_pap )

assume A1: AP is Pappian ; :: thesis: AP is satisfying_pap

let M be Subset of AP; :: according to AFF_2:def 13 :: 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 & M // N & M <> N & 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 & M // N & M <> N & 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 & M // N & M <> N & a9 in N & b9 in N & c9 in N & a,b9 // b,a9 & b,c9 // c,b9 implies a,c9 // c,a9 )

assume that

A2: M is being_line and

A3: N is being_line and

A4: a in M and

A5: b in M and

A6: c in M and

A7: M // N and

A8: M <> N 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

A14: b <> a9 by A5, A7, A8, A9, AFF_1:45;

set K = Line (a,c9);

set C = Line (c,b9);

A15: c <> b9 by A6, A7, A8, A10, AFF_1:45;

then A16: Line (c,b9) is being_line by AFF_1:24;

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

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

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

then consider T being Subset of AP such that

A26: a9 in T and

A27: Line (a,c9) // T by AFF_1:49;

A28: T is being_line by A27, AFF_1:36;

A29: c9 in Line (a,c9) by A24, AFF_1:24;

A30: ( c in Line (c,b9) & b9 in Line (c,b9) ) by A15, AFF_1:24;

not Line (c,b9) // T

A31: x in Line (c,b9) and

A32: x in T by A16, A28, AFF_1:58;

set D = Line (x,b);

A33: x <> b

then A35: Line (x,b) <> N by A5, A7, A8, AFF_1:45;

A36: Line (x,b) is being_line by A33, AFF_1:24;

A37: x in Line (x,b) by A33, AFF_1:24;

not Line (x,b) // N

A38: o in Line (x,b) and

A39: o in N by A3, A36, AFF_1:58;

LIN b9,c,x by A16, A30, A31, AFF_1:21;

then A40: b9,c // b9,x by AFF_1:def 1;

A41: a9 <> x

then A45: b,c9 // x,b9 by A13, A15, AFF_1:5;

A46: a <> b9 by A4, A7, A8, A10, AFF_1:45;

not a,b9 // Line (x,b)

A47: y in Line (x,b) and

A48: LIN a,b9,y by A36, AFF_1:59;

A49: LIN a,y,a by AFF_1:7;

A50: b9 <> x

then b9,a // b9,y by AFF_1:def 1;

then a,b9 // y,b9 by AFF_1:4;

then A55: y,b9 // b,a9 by A12, A46, AFF_1:5;

o <> b by A5, A7, A8, A39, AFF_1:45;

then y,c9 // x,a9 by A1, A3, A9, A10, A11, A36, A37, A34, A38, A39, A45, A47, A55, A35, A51, A44, A54, A42, A52;

then y,c9 // a,c9 by A43, A41, AFF_1:5;

then c9,y // c9,a by AFF_1:4;

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

then A56: LIN a,y,c9 by AFF_1:6;

LIN a,y,b9 by A48, AFF_1:6;

then ( a in Line (x,b) or a in N ) by A3, A10, A11, A23, A47, A56, A49, AFF_1:8, AFF_1:25;

then Line (x,b) // N by A2, A4, A5, A7, A8, A18, A36, A34, AFF_1:18, AFF_1:45;

hence contradiction by A38, A39, A35, AFF_1:45; :: thesis: verum

assume A1: AP is Pappian ; :: thesis: AP is satisfying_pap

let M be Subset of AP; :: according to AFF_2:def 13 :: 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 & M // N & M <> N & 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 & M // N & M <> N & 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 & M // N & M <> N & a9 in N & b9 in N & c9 in N & a,b9 // b,a9 & b,c9 // c,b9 implies a,c9 // c,a9 )

assume that

A2: M is being_line and

A3: N is being_line and

A4: a in M and

A5: b in M and

A6: c in M and

A7: M // N and

A8: M <> N 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

A14: b <> a9 by A5, A7, A8, A9, AFF_1:45;

set K = Line (a,c9);

set C = Line (c,b9);

A15: c <> b9 by A6, A7, A8, A10, AFF_1:45;

then A16: Line (c,b9) is being_line by AFF_1:24;

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

A18: now :: thesis: not a = b

assume A19:
a = b
; :: thesis: contradiction

then LIN a,b9,a9 by A12, AFF_1:def 1;

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

then ( a9 = b9 or a in N ) by A3, A9, A10, AFF_1:25;

hence contradiction by A4, A7, A8, A13, A17, A19, AFF_1:45; :: thesis: verum

end;then LIN a,b9,a9 by A12, AFF_1:def 1;

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

then ( a9 = b9 or a in N ) by A3, A9, A10, AFF_1:25;

hence contradiction by A4, A7, A8, A13, A17, A19, AFF_1:45; :: thesis: verum

A20: now :: thesis: not a9 = b9

assume
a9 = b9
; :: thesis: contradiction

then a9,a // a9,b by A12, AFF_1:4;

then LIN a9,a,b by AFF_1:def 1;

then LIN a,b,a9 by AFF_1:6;

then a9 in M by A2, A4, A5, A18, AFF_1:25;

hence contradiction by A7, A8, A9, AFF_1:45; :: thesis: verum

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

then LIN a9,a,b by AFF_1:def 1;

then LIN a,b,a9 by AFF_1:6;

then a9 in M by A2, A4, A5, A18, AFF_1:25;

hence contradiction by A7, A8, A9, AFF_1:45; :: thesis: verum

A21: now :: thesis: not b = c

assume A22:
b = c
; :: thesis: contradiction

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

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

then ( b9 = c9 or b in N ) by A3, A10, A11, AFF_1:25;

hence contradiction by A5, A7, A8, A12, A17, A22, AFF_1:45; :: thesis: verum

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

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

then ( b9 = c9 or b in N ) by A3, A10, A11, AFF_1:25;

hence contradiction by A5, A7, A8, A12, A17, A22, AFF_1:45; :: thesis: verum

A23: now :: thesis: not b9 = c9

A24:
a <> c9
by A4, A7, A8, A11, AFF_1:45;assume
b9 = c9
; :: thesis: contradiction

then b9,b // b9,c by A13, 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 A2, A5, A6, A21, AFF_1:25;

hence contradiction by A7, A8, A10, AFF_1:45; :: thesis: verum

end;then b9,b // b9,c by A13, 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 A2, A5, A6, A21, AFF_1:25;

hence contradiction by A7, A8, A10, AFF_1:45; :: thesis: verum

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

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

then consider T being Subset of AP such that

A26: a9 in T and

A27: Line (a,c9) // T by AFF_1:49;

A28: T is being_line by A27, AFF_1:36;

A29: c9 in Line (a,c9) by A24, AFF_1:24;

A30: ( c in Line (c,b9) & b9 in Line (c,b9) ) by A15, AFF_1:24;

not Line (c,b9) // T

proof

then consider x being Element of AP such that
assume
Line (c,b9) // T
; :: thesis: contradiction

then Line (c,b9) // Line (a,c9) by A27, AFF_1:44;

then c,b9 // a,c9 by A25, A29, A30, AFF_1:39;

then b,c9 // a,c9 by A13, A15, AFF_1:5;

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

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

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

then c9 in M by A2, A4, A5, A18, AFF_1:25;

hence contradiction by A7, A8, A11, AFF_1:45; :: thesis: verum

end;then Line (c,b9) // Line (a,c9) by A27, AFF_1:44;

then c,b9 // a,c9 by A25, A29, A30, AFF_1:39;

then b,c9 // a,c9 by A13, A15, AFF_1:5;

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

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

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

then c9 in M by A2, A4, A5, A18, AFF_1:25;

hence contradiction by A7, A8, A11, AFF_1:45; :: thesis: verum

A31: x in Line (c,b9) and

A32: x in T by A16, A28, AFF_1:58;

set D = Line (x,b);

A33: x <> b

proof

then A34:
b in Line (x,b)
by AFF_1:24;
assume
x = b
; :: thesis: contradiction

then LIN b,c,b9 by A16, A30, A31, AFF_1:21;

then b9 in M by A2, A5, A6, A21, AFF_1:25;

hence contradiction by A7, A8, A10, AFF_1:45; :: thesis: verum

end;then LIN b,c,b9 by A16, A30, A31, AFF_1:21;

then b9 in M by A2, A5, A6, A21, AFF_1:25;

hence contradiction by A7, A8, A10, AFF_1:45; :: thesis: verum

then A35: Line (x,b) <> N by A5, A7, A8, AFF_1:45;

A36: Line (x,b) is being_line by A33, AFF_1:24;

A37: x in Line (x,b) by A33, AFF_1:24;

not Line (x,b) // N

proof

then consider o being Element of AP such that
assume
Line (x,b) // N
; :: thesis: contradiction

then Line (x,b) // M by A7, AFF_1:44;

then x in M by A5, A37, A34, AFF_1:45;

then ( c in T or b9 in M ) by A2, A6, A16, A30, A31, A32, AFF_1:18;

hence contradiction by A7, A8, A10, A17, A25, A29, A26, A27, AFF_1:39, AFF_1:45; :: thesis: verum

end;then Line (x,b) // M by A7, AFF_1:44;

then x in M by A5, A37, A34, AFF_1:45;

then ( c in T or b9 in M ) by A2, A6, A16, A30, A31, A32, AFF_1:18;

hence contradiction by A7, A8, A10, A17, A25, A29, A26, A27, AFF_1:39, AFF_1:45; :: thesis: verum

A38: o in Line (x,b) and

A39: o in N by A3, A36, AFF_1:58;

LIN b9,c,x by A16, A30, A31, AFF_1:21;

then A40: b9,c // b9,x by AFF_1:def 1;

A41: a9 <> x

proof

assume
a9 = x
; :: thesis: contradiction

then b9,a9 // b9,c by A40, AFF_1:4;

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

then c in N by A3, A9, A10, A20, AFF_1:25;

hence contradiction by A6, A7, A8, AFF_1:45; :: thesis: verum

end;then b9,a9 // b9,c by A40, AFF_1:4;

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

then c in N by A3, A9, A10, A20, AFF_1:25;

hence contradiction by A6, A7, A8, AFF_1:45; :: thesis: verum

A42: now :: thesis: not o = x

A43:
a,c9 // x,a9
by A25, A29, A26, A27, A32, AFF_1:39;assume
o = x
; :: thesis: contradiction

then N = T by A3, A9, A26, A28, A32, A39, A41, AFF_1:18;

then N = Line (a,c9) by A11, A29, A27, AFF_1:45;

hence contradiction by A4, A7, A8, A25, AFF_1:45; :: thesis: verum

end;then N = T by A3, A9, A26, A28, A32, A39, A41, AFF_1:18;

then N = Line (a,c9) by A11, A29, A27, AFF_1:45;

hence contradiction by A4, A7, A8, A25, AFF_1:45; :: thesis: verum

A44: now :: thesis: not o = a9

c,b9 // x,b9
by A40, AFF_1:4;assume
o = a9
; :: thesis: contradiction

then LIN a9,b,x by A36, A37, A34, A38, AFF_1:21;

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

then b,a9 // x,a9 by AFF_1:4;

then a,b9 // x,a9 by A12, A14, AFF_1:5;

then a,b9 // a,c9 by A43, A41, 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 A3, A10, A11, A23, AFF_1:25;

hence contradiction by A4, A7, A8, AFF_1:45; :: thesis: verum

end;then LIN a9,b,x by A36, A37, A34, A38, AFF_1:21;

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

then b,a9 // x,a9 by AFF_1:4;

then a,b9 // x,a9 by A12, A14, AFF_1:5;

then a,b9 // a,c9 by A43, A41, 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 A3, A10, A11, A23, AFF_1:25;

hence contradiction by A4, A7, A8, AFF_1:45; :: thesis: verum

then A45: b,c9 // x,b9 by A13, A15, AFF_1:5;

A46: a <> b9 by A4, A7, A8, A10, AFF_1:45;

not a,b9 // Line (x,b)

proof

then consider y being Element of AP such that
assume
a,b9 // Line (x,b)
; :: thesis: contradiction

then b,a9 // Line (x,b) by A12, A46, AFF_1:32;

then a9 in Line (x,b) by A36, A34, AFF_1:23;

then b in T by A26, A28, A32, A36, A37, A34, A41, AFF_1:18;

then b,a9 // a,c9 by A25, A29, A26, A27, AFF_1:39;

then a,b9 // a,c9 by A12, A14, 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 A3, A10, A11, A23, AFF_1:25;

hence contradiction by A4, A7, A8, AFF_1:45; :: thesis: verum

end;then b,a9 // Line (x,b) by A12, A46, AFF_1:32;

then a9 in Line (x,b) by A36, A34, AFF_1:23;

then b in T by A26, A28, A32, A36, A37, A34, A41, AFF_1:18;

then b,a9 // a,c9 by A25, A29, A26, A27, AFF_1:39;

then a,b9 // a,c9 by A12, A14, 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 A3, A10, A11, A23, AFF_1:25;

hence contradiction by A4, A7, A8, AFF_1:45; :: thesis: verum

A47: y in Line (x,b) and

A48: LIN a,b9,y by A36, AFF_1:59;

A49: LIN a,y,a by AFF_1:7;

A50: b9 <> x

proof

assume
b9 = x
; :: thesis: contradiction

then a,c9 // a9,b9 by A25, A29, A26, A27, A32, AFF_1:39;

then a,c9 // N by A3, A9, A10, A20, AFF_1:27;

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

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

hence contradiction by A4, A7, A8, AFF_1:45; :: thesis: verum

end;then a,c9 // a9,b9 by A25, A29, A26, A27, A32, AFF_1:39;

then a,c9 // N by A3, A9, A10, A20, AFF_1:27;

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

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

hence contradiction by A4, A7, A8, AFF_1:45; :: thesis: verum

A51: now :: thesis: not o = b9

assume
o = b9
; :: thesis: contradiction

then LIN b9,x,b by A36, A37, A34, A38, AFF_1:21;

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

then x,b9 // b,b9 by AFF_1:4;

then b,c9 // b,b9 by A45, A50, AFF_1:5;

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

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

then b in N by A3, A10, A11, A23, AFF_1:25;

hence contradiction by A5, A7, A8, AFF_1:45; :: thesis: verum

end;then LIN b9,x,b by A36, A37, A34, A38, AFF_1:21;

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

then x,b9 // b,b9 by AFF_1:4;

then b,c9 // b,b9 by A45, A50, AFF_1:5;

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

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

then b in N by A3, A10, A11, A23, AFF_1:25;

hence contradiction by A5, A7, A8, AFF_1:45; :: thesis: verum

A52: now :: thesis: not o = y

A53:
b <> c9
by A5, A7, A8, A11, AFF_1:45;assume
o = y
; :: thesis: contradiction

then LIN b9,o,a by A48, AFF_1:6;

then a in N by A3, A10, A39, A51, AFF_1:25;

hence contradiction by A4, A7, A8, AFF_1:45; :: thesis: verum

end;then LIN b9,o,a by A48, AFF_1:6;

then a in N by A3, A10, A39, A51, AFF_1:25;

hence contradiction by A4, A7, A8, AFF_1:45; :: thesis: verum

A54: now :: thesis: not o = c9

LIN b9,a,y
by A48, AFF_1:6;assume
o = c9
; :: thesis: contradiction

then Line (x,b) // Line (c,b9) by A13, A15, A53, A16, A30, A36, A34, A38, AFF_1:38;

then b in Line (c,b9) by A31, A37, A34, AFF_1:45;

then LIN c,b,b9 by A16, A30, AFF_1:21;

then b9 in M by A2, A5, A6, A21, AFF_1:25;

hence contradiction by A7, A8, A10, AFF_1:45; :: thesis: verum

end;then Line (x,b) // Line (c,b9) by A13, A15, A53, A16, A30, A36, A34, A38, AFF_1:38;

then b in Line (c,b9) by A31, A37, A34, AFF_1:45;

then LIN c,b,b9 by A16, A30, AFF_1:21;

then b9 in M by A2, A5, A6, A21, AFF_1:25;

hence contradiction by A7, A8, A10, AFF_1:45; :: thesis: verum

then b9,a // b9,y by AFF_1:def 1;

then a,b9 // y,b9 by AFF_1:4;

then A55: y,b9 // b,a9 by A12, A46, AFF_1:5;

o <> b by A5, A7, A8, A39, AFF_1:45;

then y,c9 // x,a9 by A1, A3, A9, A10, A11, A36, A37, A34, A38, A39, A45, A47, A55, A35, A51, A44, A54, A42, A52;

then y,c9 // a,c9 by A43, A41, AFF_1:5;

then c9,y // c9,a by AFF_1:4;

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

then A56: LIN a,y,c9 by AFF_1:6;

LIN a,y,b9 by A48, AFF_1:6;

then ( a in Line (x,b) or a in N ) by A3, A10, A11, A23, A47, A56, A49, AFF_1:8, AFF_1:25;

then Line (x,b) // N by A2, A4, A5, A7, A8, A18, A36, A34, AFF_1:18, AFF_1:45;

hence contradiction by A38, A39, A35, AFF_1:45; :: thesis: verum