let AP be AffinPlane; :: thesis: ( AP is Desarguesian iff AP is satisfying_DES_1 )

let A be Subset of AP; :: according to AFF_2:def 4 :: thesis: for P, C being Subset of AP

for o, a, b, c, a9, b9, c9 being Element of AP st o in A & o in P & o in C & o <> a & o <> b & o <> c & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 holds

b,c // b9,c9

let P, C be Subset of AP; :: thesis: for o, a, b, c, a9, b9, c9 being Element of AP st o in A & o in P & o in C & o <> a & o <> b & o <> c & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 holds

b,c // b9,c9

let o, a, b, c, a9, b9, c9 be Element of AP; :: thesis: ( o in A & o in P & o in C & o <> a & o <> b & o <> c & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 implies b,c // b9,c9 )

assume that

A41: o in A and

A42: o in P and

A43: o in C and

A44: o <> a and

A45: o <> b and

A46: o <> c and

A47: a in A and

A48: a9 in A and

A49: b in P and

A50: b9 in P and

A51: c in C and

A52: c9 in C and

A53: A is being_line and

A54: P is being_line and

A55: C is being_line and

A56: A <> P and

A57: A <> C and

A58: a,b // a9,b9 and

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

assume A60: not b,c // b9,c9 ; :: thesis: contradiction

A61: a9 <> b9

set N = Line (b9,c9);

A68: a <> c by A41, A43, A44, A47, A51, A53, A55, A57, AFF_1:18;

then A69: c in Line (a,c) by AFF_1:24;

A70: a <> b by A41, A42, A44, A47, A49, A53, A54, A56, AFF_1:18;

A71: not LIN a9,b9,c9

then A75: ( b9 in Line (b9,c9) & c9 in Line (b9,c9) ) by AFF_1:24;

Line (b9,c9) is being_line by A74, AFF_1:24;

then consider D being Subset of AP such that

A76: b in D and

A77: Line (b9,c9) // D by AFF_1:49;

A78: a in Line (a,c) by A68, AFF_1:24;

A79: not Line (a,c) // D

D is being_line by A77, AFF_1:36;

then consider x being Element of AP such that

A81: x in Line (a,c) and

A82: x in D by A80, A79, AFF_1:58;

LIN a,c,x by A80, A78, A69, A81, AFF_1:21;

then a,c // a,x by AFF_1:def 1;

then A83: a,x // a9,c9 by A59, A68, AFF_1:5;

set T = Line (c9,x);

A84: a <> a9

A89: b,x // b9,c9 by A75, A76, A77, A82, AFF_1:39;

A90: x in Line (c9,x) by A87, AFF_1:24;

A91: a <> x

then x in C by A43, A52, A55, A66, A88, A90, AFF_1:18;

then C = Line (a,c) by A51, A55, A60, A80, A69, A81, A89, AFF_1:18;

hence contradiction by A41, A43, A44, A47, A53, A55, A57, A78, AFF_1:18; :: thesis: verum

hereby :: thesis: ( AP is satisfying_DES_1 implies AP is Desarguesian )

assume A40:
AP is satisfying_DES_1
; :: thesis: AP is Desarguesian assume A1:
AP is Desarguesian
; :: thesis: AP is satisfying_DES_1

thus AP is satisfying_DES_1 :: thesis: verum

end;thus AP is satisfying_DES_1 :: thesis: verum

proof

let A be Subset of AP; :: according to AFF_2:def 5 :: thesis: for P, C being Subset of AP

for o, a, b, c, a9, b9, c9 being Element of AP st o in A & o in P & o <> a & o <> b & o <> c & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 & b,c // b9,c9 & not LIN a,b,c & c <> c9 holds

o in C

let P, C be Subset of AP; :: thesis: for o, a, b, c, a9, b9, c9 being Element of AP st o in A & o in P & o <> a & o <> b & o <> c & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 & b,c // b9,c9 & not LIN a,b,c & c <> c9 holds

o in C

let o, a, b, c, a9, b9, c9 be Element of AP; :: thesis: ( o in A & o in P & o <> a & o <> b & o <> c & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 & b,c // b9,c9 & not LIN a,b,c & c <> c9 implies o in C )

assume that

A2: o in A and

A3: o in P and

A4: o <> a and

A5: o <> b and

o <> c and

A6: a in A and

A7: a9 in A and

A8: b in P and

A9: b9 in P and

A10: c in C and

A11: c9 in C and

A12: A is being_line and

A13: P is being_line and

A14: C is being_line and

A15: A <> P and

A16: A <> C and

A17: a,b // a9,b9 and

A18: a,c // a9,c9 and

A19: b,c // b9,c9 and

A20: not LIN a,b,c and

A21: c <> c9 ; :: thesis: o in C

set K = Line (o,c9);

assume A22: not o in C ; :: thesis: contradiction

then A23: Line (o,c9) is being_line by A11, AFF_1:24;

A24: a9 <> c9

A29: o in Line (o,c9) by A11, A22, AFF_1:24;

A30: c9 in Line (o,c9) by A11, A22, AFF_1:24;

not a,c // Line (o,c9)

A32: x in Line (o,c9) and

A33: LIN a,c,x by A23, AFF_1:59;

A34: o <> x

then a,x // a9,c9 by A18, A28, AFF_1:5;

then b,x // b9,c9 by A1, A2, A3, A4, A5, A6, A7, A8, A9, A12, A13, A15, A17, A23, A29, A30, A26, A32, A34;

then A38: b,x // b,c by A19, A36, AFF_1:5;

A39: not LIN a,b,x

then c in Line (o,c9) by A32, A39, A38, AFF_1:14;

hence contradiction by A10, A11, A14, A21, A22, A23, A29, A30, AFF_1:18; :: thesis: verum

end;for o, a, b, c, a9, b9, c9 being Element of AP st o in A & o in P & o <> a & o <> b & o <> c & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 & b,c // b9,c9 & not LIN a,b,c & c <> c9 holds

o in C

let P, C be Subset of AP; :: thesis: for o, a, b, c, a9, b9, c9 being Element of AP st o in A & o in P & o <> a & o <> b & o <> c & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 & b,c // b9,c9 & not LIN a,b,c & c <> c9 holds

o in C

let o, a, b, c, a9, b9, c9 be Element of AP; :: thesis: ( o in A & o in P & o <> a & o <> b & o <> c & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 & b,c // b9,c9 & not LIN a,b,c & c <> c9 implies o in C )

assume that

A2: o in A and

A3: o in P and

A4: o <> a and

A5: o <> b and

o <> c and

A6: a in A and

A7: a9 in A and

A8: b in P and

A9: b9 in P and

A10: c in C and

A11: c9 in C and

A12: A is being_line and

A13: P is being_line and

A14: C is being_line and

A15: A <> P and

A16: A <> C and

A17: a,b // a9,b9 and

A18: a,c // a9,c9 and

A19: b,c // b9,c9 and

A20: not LIN a,b,c and

A21: c <> c9 ; :: thesis: o in C

set K = Line (o,c9);

assume A22: not o in C ; :: thesis: contradiction

then A23: Line (o,c9) is being_line by A11, AFF_1:24;

A24: a9 <> c9

proof

A26:
A <> Line (o,c9)
assume A25:
a9 = c9
; :: thesis: contradiction

then b,c // a9,b9 by A19, AFF_1:4;

then ( a,b // b,c or a9 = b9 ) by A17, AFF_1:5;

then ( b,a // b,c or a9 = b9 ) by AFF_1:4;

then ( LIN b,a,c or a9 = b9 ) by AFF_1:def 1;

hence contradiction by A2, A3, A7, A9, A11, A12, A13, A15, A20, A22, A25, AFF_1:6, AFF_1:18; :: thesis: verum

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

then ( a,b // b,c or a9 = b9 ) by A17, AFF_1:5;

then ( b,a // b,c or a9 = b9 ) by AFF_1:4;

then ( LIN b,a,c or a9 = b9 ) by AFF_1:def 1;

hence contradiction by A2, A3, A7, A9, A11, A12, A13, A15, A20, A22, A25, AFF_1:6, AFF_1:18; :: thesis: verum

proof

A28:
a <> c
by A20, AFF_1:7;
assume
A = Line (o,c9)
; :: thesis: contradiction

then A27: c9 in A by A2, AFF_1:24;

a9,c9 // a,c by A18, AFF_1:4;

then c in A by A6, A7, A12, A24, A27, AFF_1:48;

hence contradiction by A10, A11, A12, A14, A16, A21, A27, AFF_1:18; :: thesis: verum

end;then A27: c9 in A by A2, AFF_1:24;

a9,c9 // a,c by A18, AFF_1:4;

then c in A by A6, A7, A12, A24, A27, AFF_1:48;

hence contradiction by A10, A11, A12, A14, A16, A21, A27, AFF_1:18; :: thesis: verum

A29: o in Line (o,c9) by A11, A22, AFF_1:24;

A30: c9 in Line (o,c9) by A11, A22, AFF_1:24;

not a,c // Line (o,c9)

proof

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

then a9,c9 // Line (o,c9) by A18, A28, AFF_1:32;

then c9,a9 // Line (o,c9) by AFF_1:34;

then a9 in Line (o,c9) by A23, A30, AFF_1:23;

then A31: a9 in P by A2, A3, A7, A12, A23, A29, A26, AFF_1:18;

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

then ( a9 = b9 or a in P ) by A8, A9, A13, A31, AFF_1:48;

then a,c // b,c by A2, A3, A4, A6, A12, A13, A15, A18, A19, A24, AFF_1:5, AFF_1:18;

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

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

hence contradiction by A20, AFF_1:6; :: thesis: verum

end;then a9,c9 // Line (o,c9) by A18, A28, AFF_1:32;

then c9,a9 // Line (o,c9) by AFF_1:34;

then a9 in Line (o,c9) by A23, A30, AFF_1:23;

then A31: a9 in P by A2, A3, A7, A12, A23, A29, A26, AFF_1:18;

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

then ( a9 = b9 or a in P ) by A8, A9, A13, A31, AFF_1:48;

then a,c // b,c by A2, A3, A4, A6, A12, A13, A15, A18, A19, A24, AFF_1:5, AFF_1:18;

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

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

hence contradiction by A20, AFF_1:6; :: thesis: verum

A32: x in Line (o,c9) and

A33: LIN a,c,x by A23, AFF_1:59;

A34: o <> x

proof

A36:
b9 <> c9
assume
o = x
; :: thesis: contradiction

then LIN a,o,c by A33, AFF_1:6;

then A35: c in A by A2, A4, A6, A12, AFF_1:25;

then c9 in A by A6, A7, A12, A18, A28, AFF_1:48;

hence contradiction by A10, A11, A12, A14, A16, A21, A35, AFF_1:18; :: thesis: verum

end;then LIN a,o,c by A33, AFF_1:6;

then A35: c in A by A2, A4, A6, A12, AFF_1:25;

then c9 in A by A6, A7, A12, A18, A28, AFF_1:48;

hence contradiction by A10, A11, A12, A14, A16, A21, A35, AFF_1:18; :: thesis: verum

proof

A37:
a,c // a,x
by A33, AFF_1:def 1;
assume
b9 = c9
; :: thesis: contradiction

then ( a9 = b9 or a,c // a,b ) by A17, A18, AFF_1:5;

then ( a9 = b9 or LIN a,c,b ) by AFF_1:def 1;

then b,c // a,c by A18, A19, A20, A24, AFF_1:5, AFF_1:6;

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

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

hence contradiction by A20, AFF_1:6; :: thesis: verum

end;then ( a9 = b9 or a,c // a,b ) by A17, A18, AFF_1:5;

then ( a9 = b9 or LIN a,c,b ) by AFF_1:def 1;

then b,c // a,c by A18, A19, A20, A24, AFF_1:5, AFF_1:6;

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

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

hence contradiction by A20, AFF_1:6; :: thesis: verum

then a,x // a9,c9 by A18, A28, AFF_1:5;

then b,x // b9,c9 by A1, A2, A3, A4, A5, A6, A7, A8, A9, A12, A13, A15, A17, A23, A29, A30, A26, A32, A34;

then A38: b,x // b,c by A19, A36, AFF_1:5;

A39: not LIN a,b,x

proof

LIN a,x,c
by A33, AFF_1:6;
assume
LIN a,b,x
; :: thesis: contradiction

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

then ( a,b // a,c or a = x ) by A37, AFF_1:5;

hence contradiction by A2, A4, A6, A12, A20, A23, A29, A26, A32, AFF_1:18, AFF_1:def 1; :: thesis: verum

end;then a,b // a,x by AFF_1:def 1;

then ( a,b // a,c or a = x ) by A37, AFF_1:5;

hence contradiction by A2, A4, A6, A12, A20, A23, A29, A26, A32, AFF_1:18, AFF_1:def 1; :: thesis: verum

then c in Line (o,c9) by A32, A39, A38, AFF_1:14;

hence contradiction by A10, A11, A14, A21, A22, A23, A29, A30, AFF_1:18; :: thesis: verum

let A be Subset of AP; :: according to AFF_2:def 4 :: thesis: for P, C being Subset of AP

for o, a, b, c, a9, b9, c9 being Element of AP st o in A & o in P & o in C & o <> a & o <> b & o <> c & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 holds

b,c // b9,c9

let P, C be Subset of AP; :: thesis: for o, a, b, c, a9, b9, c9 being Element of AP st o in A & o in P & o in C & o <> a & o <> b & o <> c & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 holds

b,c // b9,c9

let o, a, b, c, a9, b9, c9 be Element of AP; :: thesis: ( o in A & o in P & o in C & o <> a & o <> b & o <> c & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 implies b,c // b9,c9 )

assume that

A41: o in A and

A42: o in P and

A43: o in C and

A44: o <> a and

A45: o <> b and

A46: o <> c and

A47: a in A and

A48: a9 in A and

A49: b in P and

A50: b9 in P and

A51: c in C and

A52: c9 in C and

A53: A is being_line and

A54: P is being_line and

A55: C is being_line and

A56: A <> P and

A57: A <> C and

A58: a,b // a9,b9 and

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

assume A60: not b,c // b9,c9 ; :: thesis: contradiction

A61: a9 <> b9

proof

A64:
a9 <> c9
A62:
a9,c9 // c,a
by A59, AFF_1:4;

assume A63: a9 = b9 ; :: thesis: contradiction

then a9 in C by A41, A42, A43, A48, A50, A53, A54, A56, AFF_1:18;

then ( a in C or a9 = c9 ) by A51, A52, A55, A62, AFF_1:48;

hence contradiction by A41, A43, A44, A47, A53, A55, A57, A60, A63, AFF_1:3, AFF_1:18; :: thesis: verum

end;assume A63: a9 = b9 ; :: thesis: contradiction

then a9 in C by A41, A42, A43, A48, A50, A53, A54, A56, AFF_1:18;

then ( a in C or a9 = c9 ) by A51, A52, A55, A62, AFF_1:48;

hence contradiction by A41, A43, A44, A47, A53, A55, A57, A60, A63, AFF_1:3, AFF_1:18; :: thesis: verum

proof

A66:
o <> c9
assume
a9 = c9
; :: thesis: contradiction

then A65: a9 in P by A41, A42, A43, A48, A52, A53, A55, A57, AFF_1:18;

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

then a in P by A49, A50, A54, A61, A65, AFF_1:48;

hence contradiction by A41, A42, A44, A47, A53, A54, A56, AFF_1:18; :: thesis: verum

end;then A65: a9 in P by A41, A42, A43, A48, A52, A53, A55, A57, AFF_1:18;

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

then a in P by A49, A50, A54, A61, A65, AFF_1:48;

hence contradiction by A41, A42, A44, A47, A53, A54, A56, AFF_1:18; :: thesis: verum

proof

set M = Line (a,c);
assume A67:
o = c9
; :: thesis: contradiction

a9,c9 // a,c by A59, AFF_1:4;

then c in A by A41, A47, A48, A53, A64, A67, AFF_1:48;

hence contradiction by A41, A43, A46, A51, A53, A55, A57, AFF_1:18; :: thesis: verum

end;a9,c9 // a,c by A59, AFF_1:4;

then c in A by A41, A47, A48, A53, A64, A67, AFF_1:48;

hence contradiction by A41, A43, A46, A51, A53, A55, A57, AFF_1:18; :: thesis: verum

set N = Line (b9,c9);

A68: a <> c by A41, A43, A44, A47, A51, A53, A55, A57, AFF_1:18;

then A69: c in Line (a,c) by AFF_1:24;

A70: a <> b by A41, A42, A44, A47, A49, A53, A54, A56, AFF_1:18;

A71: not LIN a9,b9,c9

proof

A74:
b9 <> c9
by A60, AFF_1:3;
assume A72:
LIN a9,b9,c9
; :: thesis: contradiction

then a9,b9 // a9,c9 by AFF_1:def 1;

then a9,b9 // a,c by A59, A64, AFF_1:5;

then a,b // a,c by A58, A61, AFF_1:5;

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

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

then b,c // b,a by AFF_1:def 1;

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

then A73: b,c // a9,b9 by A58, A70, AFF_1:5;

LIN b9,c9,a9 by A72, AFF_1:6;

then b9,c9 // b9,a9 by AFF_1:def 1;

then b9,c9 // a9,b9 by AFF_1:4;

hence contradiction by A60, A61, A73, AFF_1:5; :: thesis: verum

end;then a9,b9 // a9,c9 by AFF_1:def 1;

then a9,b9 // a,c by A59, A64, AFF_1:5;

then a,b // a,c by A58, A61, AFF_1:5;

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

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

then b,c // b,a by AFF_1:def 1;

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

then A73: b,c // a9,b9 by A58, A70, AFF_1:5;

LIN b9,c9,a9 by A72, AFF_1:6;

then b9,c9 // b9,a9 by AFF_1:def 1;

then b9,c9 // a9,b9 by AFF_1:4;

hence contradiction by A60, A61, A73, AFF_1:5; :: thesis: verum

then A75: ( b9 in Line (b9,c9) & c9 in Line (b9,c9) ) by AFF_1:24;

Line (b9,c9) is being_line by A74, AFF_1:24;

then consider D being Subset of AP such that

A76: b in D and

A77: Line (b9,c9) // D by AFF_1:49;

A78: a in Line (a,c) by A68, AFF_1:24;

A79: not Line (a,c) // D

proof

A80:
Line (a,c) is being_line
by A68, AFF_1:24;
assume
Line (a,c) // D
; :: thesis: contradiction

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

then a,c // b9,c9 by A78, A69, A75, AFF_1:39;

then a9,c9 // b9,c9 by A59, A68, AFF_1:5;

then c9,a9 // c9,b9 by AFF_1:4;

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

hence contradiction by A71, AFF_1:6; :: thesis: verum

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

then a,c // b9,c9 by A78, A69, A75, AFF_1:39;

then a9,c9 // b9,c9 by A59, A68, AFF_1:5;

then c9,a9 // c9,b9 by AFF_1:4;

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

hence contradiction by A71, AFF_1:6; :: thesis: verum

D is being_line by A77, AFF_1:36;

then consider x being Element of AP such that

A81: x in Line (a,c) and

A82: x in D by A80, A79, AFF_1:58;

LIN a,c,x by A80, A78, A69, A81, AFF_1:21;

then a,c // a,x by AFF_1:def 1;

then A83: a,x // a9,c9 by A59, A68, AFF_1:5;

set T = Line (c9,x);

A84: a <> a9

proof

A87:
x <> c9
assume A85:
a = a9
; :: thesis: contradiction

then LIN a,c,c9 by A59, AFF_1:def 1;

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

then A86: ( c = c9 or a in C ) by A51, A52, A55, AFF_1:25;

LIN a,b,b9 by A58, A85, AFF_1:def 1;

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

then ( b = b9 or a in P ) by A49, A50, A54, AFF_1:25;

hence contradiction by A41, A42, A43, A44, A47, A53, A54, A55, A56, A57, A60, A86, AFF_1:2, AFF_1:18; :: thesis: verum

end;then LIN a,c,c9 by A59, AFF_1:def 1;

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

then A86: ( c = c9 or a in C ) by A51, A52, A55, AFF_1:25;

LIN a,b,b9 by A58, A85, AFF_1:def 1;

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

then ( b = b9 or a in P ) by A49, A50, A54, AFF_1:25;

hence contradiction by A41, A42, A43, A44, A47, A53, A54, A55, A56, A57, A60, A86, AFF_1:2, AFF_1:18; :: thesis: verum

proof

then A88:
( Line (c9,x) is being_line & c9 in Line (c9,x) )
by AFF_1:24;
assume
x = c9
; :: thesis: contradiction

then c9,a // c9,a9 by A83, AFF_1:4;

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

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

then c9 in A by A47, A48, A53, A84, AFF_1:25;

hence contradiction by A41, A43, A52, A53, A55, A57, A66, AFF_1:18; :: thesis: verum

end;then c9,a // c9,a9 by A83, AFF_1:4;

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

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

then c9 in A by A47, A48, A53, A84, AFF_1:25;

hence contradiction by A41, A43, A52, A53, A55, A57, A66, AFF_1:18; :: thesis: verum

A89: b,x // b9,c9 by A75, A76, A77, A82, AFF_1:39;

A90: x in Line (c9,x) by A87, AFF_1:24;

A91: a <> x

proof

not LIN a,b,x
assume
a = x
; :: thesis: contradiction

then a,b // b9,c9 by A75, A76, A77, A82, AFF_1:39;

then a9,b9 // b9,c9 by A58, A70, AFF_1:5;

then b9,a9 // b9,c9 by AFF_1:4;

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

hence contradiction by A71, AFF_1:6; :: thesis: verum

end;then a,b // b9,c9 by A75, A76, A77, A82, AFF_1:39;

then a9,b9 // b9,c9 by A58, A70, AFF_1:5;

then b9,a9 // b9,c9 by AFF_1:4;

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

hence contradiction by A71, AFF_1:6; :: thesis: verum

proof

then
o in Line (c9,x)
by A40, A41, A42, A44, A45, A47, A48, A49, A50, A53, A54, A56, A58, A83, A89, A87, A88, A90;
assume
LIN a,b,x
; :: thesis: contradiction

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

then a,b // a9,c9 by A83, A91, AFF_1:5;

then a9,b9 // a9,c9 by A58, A70, AFF_1:5;

hence contradiction by A71, AFF_1:def 1; :: thesis: verum

end;then a,b // a,x by AFF_1:def 1;

then a,b // a9,c9 by A83, A91, AFF_1:5;

then a9,b9 // a9,c9 by A58, A70, AFF_1:5;

hence contradiction by A71, AFF_1:def 1; :: thesis: verum

then x in C by A43, A52, A55, A66, A88, A90, AFF_1:18;

then C = Line (a,c) by A51, A55, A60, A80, A69, A81, A89, AFF_1:18;

hence contradiction by A41, A43, A44, A47, A53, A55, A57, A78, AFF_1:18; :: thesis: verum