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

A1: now

assume A2: AP is satisfying_DES_1 ; :: thesis: AP is Desarguesian
thus AP is Desarguesian :: thesis: verum

proof

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
A3: o in A and
A4: o in P and
A5: o in C and
A6: o <> a and
A7: o <> b and
A8: o <> c and
A9: a in A and
A10: a9 in A and
A11: b in P and
A12: b9 in P and
A13: c in C and
A14: c9 in C and
A15: A is being_line and
A16: P is being_line and
A17: C is being_line and
A18: A <> P and
A19: A <> C and
A20: a,b // a9,b9 and
A21: a,c // a9,c9 ; :: thesis: b,c // b9,c9
assume A22: not b,c // b9,c9 ; :: thesis: contradiction
A23: a9 <> b9

proof

A24: a9,c9 // c,a by A21, AFF_1:13;
assume A25: a9 = b9 ; :: thesis: contradiction
then a9 in C by A3, A4, A5, A10, A12, A15, A16, A18, AFF_1:30;
then ( a in C or a9 = c9 ) by A13, A14, A17, A24, AFF_1:62;
hence contradiction by A3, A5, A6, A9, A15, A17, A19, A22, A25, AFF_1:12, AFF_1:30; :: thesis: verum

end;

A26: a9 <> c9

proof

assume a9 = c9 ; :: thesis: contradiction
then A27: a9 in P by A3, A4, A5, A10, A14, A15, A17, A19, AFF_1:30;
a9,b9 // b,a by A20, AFF_1:13;
then a in P by A11, A12, A16, A23, A27, AFF_1:62;
hence contradiction by A3, A4, A6, A9, A15, A16, A18, AFF_1:30; :: thesis: verum

end;

A28: o <> c9

proof

assume A29: o = c9 ; :: thesis: contradiction
a9,c9 // a,c by A21, AFF_1:13;
then c in A by A3, A9, A10, A15, A26, A29, AFF_1:62;
hence contradiction by A3, A5, A8, A13, A15, A17, A19, AFF_1:30; :: thesis: verum

end;

set K = Line a9,c9;
set M = Line a,c;
set N = Line b9,c9;
A30: a <> c by A3, A5, A6, A9, A13, A15, A17, A19, AFF_1:30;
then A31: c in Line a,c by AFF_1:38;
A32: a <> b by A3, A4, A6, A9, A11, A15, A16, A18, AFF_1:30;
A33: not LIN a9,b9,c9

proof

assume A34: LIN a9,b9,c9 ; :: thesis: contradiction
then a9,b9 // a9,c9 by AFF_1:def 1;
then a9,b9 // a,c by A21, A26, AFF_1:14;
then a,b // a,c by A20, A23, AFF_1:14;
then LIN a,b,c by AFF_1:def 1;
then LIN b,c,a by AFF_1:15;
then b,c // b,a by AFF_1:def 1;
then b,c // a,b by AFF_1:13;
then A35: b,c // a9,b9 by A20, A32, AFF_1:14;
LIN b9,c9,a9 by A34, AFF_1:15;
then b9,c9 // b9,a9 by AFF_1:def 1;
then b9,c9 // a9,b9 by AFF_1:13;
hence contradiction by A22, A23, A35, AFF_1:14; :: thesis: verum

end;

A36: b9 <> c9 by A22, AFF_1:12;
then A37: ( b9 in Line b9,c9 & c9 in Line b9,c9 ) by AFF_1:38;
Line b9,c9 is being_line by A36, AFF_1:38;
then consider D being Subset of AP such that
A38: b in D and
A39: Line b9,c9 // D by AFF_1:63;
A40: a in Line a,c by A30, AFF_1:38;
A41: not Line a,c // D

proof

assume Line a,c // D ; :: thesis: contradiction
then Line a,c // Line b9,c9 by A39, AFF_1:58;
then a,c // b9,c9 by A40, A31, A37, AFF_1:53;
then a9,c9 // b9,c9 by A21, A30, AFF_1:14;
then c9,a9 // c9,b9 by AFF_1:13;
then LIN c9,a9,b9 by AFF_1:def 1;
hence contradiction by A33, AFF_1:15; :: thesis: verum

end;

A42: Line a,c is being_line by A30, AFF_1:38;
D is being_line by A39, AFF_1:50;
then consider x being Element of AP such that
A43: x in Line a,c and
A44: x in D by A42, A41, AFF_1:72;
LIN a,c,x by A42, A40, A31, A43, AFF_1:33;
then a,c // a,x by AFF_1:def 1;
then A45: a,x // a9,c9 by A21, A30, AFF_1:14;
set T = Line c9,x;
A46: a <> a9

proof

assume A47: a = a9 ; :: thesis: contradiction
then LIN a,c,c9 by A21, AFF_1:def 1;
then LIN c,c9,a by AFF_1:15;
then A48: ( c = c9 or a in C ) by A13, A14, A17, AFF_1:39;
LIN a,b,b9 by A20, A47, AFF_1:def 1;
then LIN b,b9,a by AFF_1:15;
then ( b = b9 or a in P ) by A11, A12, A16, AFF_1:39;
hence contradiction by A3, A4, A5, A6, A9, A15, A16, A17, A18, A19, A22, A48, AFF_1:11, AFF_1:30; :: thesis: verum

end;

A49: x <> c9

proof

assume x = c9 ; :: thesis: contradiction
then c9,a // c9,a9 by A45, AFF_1:13;
then LIN c9,a,a9 by AFF_1:def 1;
then LIN a,a9,c9 by AFF_1:15;
then c9 in A by A9, A10, A15, A46, AFF_1:39;
hence contradiction by A3, A5, A14, A15, A17, A19, A28, AFF_1:30; :: thesis: verum

end;

then A50: ( Line c9,x is being_line & c9 in Line c9,x ) by AFF_1:38;
A51: b,x // b9,c9 by A37, A38, A39, A44, AFF_1:53;
A52: x in Line c9,x by A49, AFF_1:38;
A53: a <> x

proof

assume a = x ; :: thesis: contradiction
then a,b // b9,c9 by A37, A38, A39, A44, AFF_1:53;
then a9,b9 // b9,c9 by A20, A32, AFF_1:14;
then b9,a9 // b9,c9 by AFF_1:13;
then LIN b9,a9,c9 by AFF_1:def 1;
hence contradiction by A33, AFF_1:15; :: thesis: verum

end;

not LIN a,b,x

proof

assume LIN a,b,x ; :: thesis: contradiction
then a,b // a,x by AFF_1:def 1;
then a,b // a9,c9 by A45, A53, AFF_1:14;
then a9,b9 // a9,c9 by A20, A32, AFF_1:14;
hence contradiction by A33, AFF_1:def 1; :: thesis: verum

end;

then o in Line c9,x by A2, A3, A4, A6, A7, A9, A10, A11, A12, A15, A16, A18, A20, A45, A51, A49, A50, A52, Def5;
then x in C by A5, A14, A17, A28, A50, A52, AFF_1:30;
then C = Line a,c by A13, A17, A22, A42, A31, A43, A51, AFF_1:30;
hence contradiction by A3, A5, A6, A9, A15, A17, A19, A40, AFF_1:30; :: thesis: verum

end;

end;

now

assume A54: AP is Desarguesian ; :: thesis: AP is satisfying_DES_1
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
A55: o in A and
A56: o in P and
A57: o <> a and
A58: o <> b and
o <> c and
A59: a in A and
A60: a9 in A and
A61: b in P and
A62: b9 in P and
A63: c in C and
A64: c9 in C and
A65: A is being_line and
A66: P is being_line and
A67: C is being_line and
A68: A <> P and
A69: A <> C and
A70: a,b // a9,b9 and
A71: a,c // a9,c9 and
A72: b,c // b9,c9 and
A73: not LIN a,b,c and
A74: c <> c9 ; :: thesis: o in C
set K = Line o,c9;
assume A75: not o in C ; :: thesis: contradiction
then A76: Line o,c9 is being_line by A64, AFF_1:38;
A77: a9 <> c9

proof

assume A78: a9 = c9 ; :: thesis: contradiction
then b,c // a9,b9 by A72, AFF_1:13;
then ( a,b // b,c or a9 = b9 ) by A70, AFF_1:14;
then ( b,a // b,c or a9 = b9 ) by AFF_1:13;
then ( LIN b,a,c or a9 = b9 ) by AFF_1:def 1;
hence contradiction by A55, A56, A60, A62, A64, A65, A66, A68, A73, A75, A78, AFF_1:15, AFF_1:30; :: thesis: verum

end;

A79: A <> Line o,c9

proof

assume A = Line o,c9 ; :: thesis: contradiction
then A80: c9 in A by A55, AFF_1:38;
a9,c9 // a,c by A71, AFF_1:13;
then c in A by A59, A60, A65, A77, A80, AFF_1:62;
hence contradiction by A63, A64, A65, A67, A69, A74, A80, AFF_1:30; :: thesis: verum

end;

A81: a <> c by A73, AFF_1:16;
A82: o in Line o,c9 by A64, A75, AFF_1:38;
A83: c9 in Line o,c9 by A64, A75, AFF_1:38;
not a,c // Line o,c9

proof

assume a,c // Line o,c9 ; :: thesis: contradiction
then a9,c9 // Line o,c9 by A71, A81, AFF_1:46;
then c9,a9 // Line o,c9 by AFF_1:48;
then a9 in Line o,c9 by A76, A83, AFF_1:37;
then A84: a9 in P by A55, A56, A60, A65, A76, A82, A79, AFF_1:30;
a9,b9 // b,a by A70, AFF_1:13;
then ( a9 = b9 or a in P ) by A61, A62, A66, A84, AFF_1:62;
then a,c // b,c by A55, A56, A57, A59, A65, A66, A68, A71, A72, A77, AFF_1:14, AFF_1:30;
then c,a // c,b by AFF_1:13;
then LIN c,a,b by AFF_1:def 1;
hence contradiction by A73, AFF_1:15; :: thesis: verum

end;

then consider x being Element of AP such that
A85: x in Line o,c9 and
A86: LIN a,c,x by A76, AFF_1:73;
A87: o <> x

proof

assume o = x ; :: thesis: contradiction
then LIN a,o,c by A86, AFF_1:15;
then A88: c in A by A55, A57, A59, A65, AFF_1:39;
then c9 in A by A59, A60, A65, A71, A81, AFF_1:62;
hence contradiction by A63, A64, A65, A67, A69, A74, A88, AFF_1:30; :: thesis: verum

end;

A89: b9 <> c9

proof

assume b9 = c9 ; :: thesis: contradiction
then ( a9 = b9 or a,c // a,b ) by A70, A71, AFF_1:14;
then ( a9 = b9 or LIN a,c,b ) by AFF_1:def 1;
then b,c // a,c by A71, A72, A73, A77, AFF_1:14, AFF_1:15;
then c,b // c,a by AFF_1:13;
then LIN c,b,a by AFF_1:def 1;
hence contradiction by A73, AFF_1:15; :: thesis: verum

end;

A90: a,c // a,x by A86, AFF_1:def 1;
then a,x // a9,c9 by A71, A81, AFF_1:14;
then b,x // b9,c9 by A54, A55, A56, A57, A58, A59, A60, A61, A62, A65, A66, A68, A70, A76, A82, A83, A79, A85, A87, Def4;
then A91: b,x // b,c by A72, A89, AFF_1:14;
A92: not LIN a,b,x

proof

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 A90, AFF_1:14;
hence contradiction by A55, A57, A59, A65, A73, A76, A82, A79, A85, AFF_1:30, AFF_1:def 1; :: thesis: verum

end;

LIN a,x,c by A86, AFF_1:15;
then c in Line o,c9 by A85, A92, A91, AFF_1:23;
hence contradiction by A63, A64, A67, A74, A75, A76, A82, A83, AFF_1:30; :: thesis: verum

end;

end;

hence ( AP is Desarguesian iff AP is satisfying_DES_1 ) by A1; :: thesis: verum