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 ; :: according to AFF_2:def 4 :: thesis: for P, C being Subset of
for o, a, b, c, a', b', c' being Element of st o in A & o in P & o in C & o <> a & o <> b & o <> c & a in A & a' in A & b in P & b' in P & c in C & c' in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a',b' & a,c // a',c' holds
b,c // b',c'
let P, C be Subset of ; :: thesis: for o, a, b, c, a', b', c' being Element of st o in A & o in P & o in C & o <> a & o <> b & o <> c & a in A & a' in A & b in P & b' in P & c in C & c' in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a',b' & a,c // a',c' holds
b,c // b',c'
let o, a, b, c, a', b', c' be Element of ; :: thesis: ( o in A & o in P & o in C & o <> a & o <> b & o <> c & a in A & a' in A & b in P & b' in P & c in C & c' in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a',b' & a,c // a',c' implies b,c // b',c' )
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: a' in A and
A11: b in P and
A12: b' in P and
A13: c in C and
A14: c' 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 // a',b' and
A21: a,c // a',c' ; :: thesis: b,c // b',c'
assume A22: not b,c // b',c' ; :: thesis: contradiction
A23: a' <> b'

proof

A24: a',c' // c,a by A21, AFF_1:13;
assume A25: a' = b' ; :: thesis: contradiction
then a' in C by A3, A4, A5, A10, A12, A15, A16, A18, AFF_1:30;
then ( a in C or a' = c' ) 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: a' <> c'

proof

assume a' = c' ; :: thesis: contradiction
then A27: a' in P by A3, A4, A5, A10, A14, A15, A17, A19, AFF_1:30;
a',b' // 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 <> c'

proof

assume A29: o = c' ; :: thesis: contradiction
a',c' // 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 a',c';
set M = Line a,c;
set N = Line b',c';
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 a',b',c'

proof

assume A34: LIN a',b',c' ; :: thesis: contradiction
then a',b' // a',c' by AFF_1:def 1;
then a',b' // 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 // a',b' by A20, A32, AFF_1:14;
LIN b',c',a' by A34, AFF_1:15;
then b',c' // b',a' by AFF_1:def 1;
then b',c' // a',b' by AFF_1:13;
hence contradiction by A22, A23, A35, AFF_1:14; :: thesis: verum

end;

A36: b' <> c' by A22, AFF_1:12;
then A37: ( b' in Line b',c' & c' in Line b',c' ) by AFF_1:38;
Line b',c' is being_line by A36, AFF_1:38;
then consider D being Subset of such that
A38: b in D and
A39: Line b',c' // 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 b',c' by A39, AFF_1:58;
then a,c // b',c' by A40, A31, A37, AFF_1:53;
then a',c' // b',c' by A21, A30, AFF_1:14;
then c',a' // c',b' by AFF_1:13;
then LIN c',a',b' 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 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 // a',c' by A21, A30, AFF_1:14;
set T = Line c',x;
A46: a <> a'

proof

assume A47: a = a' ; :: thesis: contradiction
then LIN a,c,c' by A21, AFF_1:def 1;
then LIN c,c',a by AFF_1:15;
then A48: ( c = c' or a in C ) by A13, A14, A17, AFF_1:39;
LIN a,b,b' by A20, A47, AFF_1:def 1;
then LIN b,b',a by AFF_1:15;
then ( b = b' 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 <> c'

proof

assume x = c' ; :: thesis: contradiction
then c',a // c',a' by A45, AFF_1:13;
then LIN c',a,a' by AFF_1:def 1;
then LIN a,a',c' by AFF_1:15;
then c' 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 c',x is being_line & c' in Line c',x ) by AFF_1:38;
A51: b,x // b',c' by A37, A38, A39, A44, AFF_1:53;
A52: x in Line c',x by A49, AFF_1:38;
A53: a <> x

proof

assume a = x ; :: thesis: contradiction
then a,b // b',c' by A37, A38, A39, A44, AFF_1:53;
then a',b' // b',c' by A20, A32, AFF_1:14;
then b',a' // b',c' by AFF_1:13;
then LIN b',a',c' 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 // a',c' by A45, A53, AFF_1:14;
then a',b' // a',c' by A20, A32, AFF_1:14;
hence contradiction by A33, AFF_1:def 1; :: thesis: verum

end;

then o in Line c',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 ; :: according to AFF_2:def 5 :: thesis: for P, C being Subset of
for o, a, b, c, a', b', c' being Element of st o in A & o in P & o <> a & o <> b & o <> c & a in A & a' in A & b in P & b' in P & c in C & c' in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a',b' & a,c // a',c' & b,c // b',c' & not LIN a,b,c & c <> c' holds
o in C
let P, C be Subset of ; :: thesis: for o, a, b, c, a', b', c' being Element of st o in A & o in P & o <> a & o <> b & o <> c & a in A & a' in A & b in P & b' in P & c in C & c' in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a',b' & a,c // a',c' & b,c // b',c' & not LIN a,b,c & c <> c' holds
o in C
let o, a, b, c, a', b', c' be Element of ; :: thesis: ( o in A & o in P & o <> a & o <> b & o <> c & a in A & a' in A & b in P & b' in P & c in C & c' in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a',b' & a,c // a',c' & b,c // b',c' & not LIN a,b,c & c <> c' 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: a' in A and
A61: b in P and
A62: b' in P and
A63: c in C and
A64: c' 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 // a',b' and
A71: a,c // a',c' and
A72: b,c // b',c' and
A73: not LIN a,b,c and
A74: c <> c' ; :: thesis: o in C
set K = Line o,c';
assume A75: not o in C ; :: thesis: contradiction
then A76: Line o,c' is being_line by A64, AFF_1:38;
A77: a' <> c'

proof

assume A78: a' = c' ; :: thesis: contradiction
then b,c // a',b' by A72, AFF_1:13;
then ( a,b // b,c or a' = b' ) by A70, AFF_1:14;
then ( b,a // b,c or a' = b' ) by AFF_1:13;
then ( LIN b,a,c or a' = b' ) 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,c'

proof

assume A = Line o,c' ; :: thesis: contradiction
then A80: c' in A by A55, AFF_1:38;
a',c' // 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,c' by A64, A75, AFF_1:38;
A83: c' in Line o,c' by A64, A75, AFF_1:38;
not a,c // Line o,c'

proof

assume a,c // Line o,c' ; :: thesis: contradiction
then a',c' // Line o,c' by A71, A81, AFF_1:46;
then c',a' // Line o,c' by AFF_1:48;
then a' in Line o,c' by A76, A83, AFF_1:37;
then A84: a' in P by A55, A56, A60, A65, A76, A82, A79, AFF_1:30;
a',b' // b,a by A70, AFF_1:13;
then ( a' = b' 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 such that
A85: x in Line o,c' 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 c' 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: b' <> c'

proof

assume b' = c' ; :: thesis: contradiction
then ( a' = b' or a,c // a,b ) by A70, A71, AFF_1:14;
then ( a' = b' 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 // a',c' by A71, A81, AFF_1:14;
then b,x // b',c' 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,c' 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