let X be AffinPlane; :: thesis: ( X is Desarguesian iff X is satisfying_Scherungssatz )
A1: ( X is satisfying_Scherungssatz implies X is Desarguesian )

proof

assume A2: X is satisfying_Scherungssatz ; :: thesis: X is Desarguesian

now

let Y, Z, M be Subset of X; :: thesis: for o, a, b, c, a1, b1, c1 being Element of X st o in Y & o in Z & o in M & o <> a & o <> b & o <> c & a in Y & a1 in Y & b in Z & b1 in Z & c in M & c1 in M & Y is being_line & Z is being_line & M is being_line & Y <> Z & Y <> M & a,b // a1,b1 & a,c // a1,c1 holds
b,c // b1,c1
let o, a, b, c, a1, b1, c1 be Element of X; :: thesis: ( o in Y & o in Z & o in M & o <> a & o <> b & o <> c & a in Y & a1 in Y & b in Z & b1 in Z & c in M & c1 in M & Y is being_line & Z is being_line & M is being_line & Y <> Z & Y <> M & a,b // a1,b1 & a,c // a1,c1 implies b,c // b1,c1 )
assume A3: ( o in Y & o in Z & o in M & o <> a & o <> b & o <> c & a in Y & a1 in Y & b in Z & b1 in Z & c in M & c1 in M & Y is being_line & Z is being_line & M is being_line & Y <> Z & Y <> M & a,b // a1,b1 & a,c // a1,c1 ) ; :: thesis: b,c // b1,c1
assume A4: not b,c // b1,c1 ; :: thesis: contradiction

A5: now

let Y, Z, M be Subset of X; :: thesis: for o, a, b, c, a1, b1, c1, d being Element of X st X is satisfying_Scherungssatz & o in Y & o in Z & o in M & o <> a & o <> b & o <> c & a in Y & a1 in Y & b in Z & b1 in Z & c in M & c1 in M & Y is being_line & Z is being_line & M is being_line & Y <> Z & Y <> M & a,b // a1,b1 & a,c // a1,c1 & LIN b,c,d & LIN b1,c1,d & not LIN a,a1,d holds
b,c // b1,c1
let o, a, b, c, a1, b1, c1, d be Element of X; :: thesis: ( X is satisfying_Scherungssatz & o in Y & o in Z & o in M & o <> a & o <> b & o <> c & a in Y & a1 in Y & b in Z & b1 in Z & c in M & c1 in M & Y is being_line & Z is being_line & M is being_line & Y <> Z & Y <> M & a,b // a1,b1 & a,c // a1,c1 & LIN b,c,d & LIN b1,c1,d & not LIN a,a1,d implies b,c // b1,c1 )
assume A6: X is satisfying_Scherungssatz ; :: thesis: ( o in Y & o in Z & o in M & o <> a & o <> b & o <> c & a in Y & a1 in Y & b in Z & b1 in Z & c in M & c1 in M & Y is being_line & Z is being_line & M is being_line & Y <> Z & Y <> M & a,b // a1,b1 & a,c // a1,c1 & LIN b,c,d & LIN b1,c1,d & not LIN a,a1,d implies b,c // b1,c1 )
assume A7: ( o in Y & o in Z & o in M & o <> a & o <> b & o <> c & a in Y & a1 in Y & b in Z & b1 in Z & c in M & c1 in M & Y is being_line & Z is being_line & M is being_line & Y <> Z & Y <> M & a,b // a1,b1 & a,c // a1,c1 & LIN b,c,d & LIN b1,c1,d ) ; :: thesis: ( LIN a,a1,d or b,c // b1,c1 )
( LIN a,a1,d or b,c // b1,c1 )

proof

assume A8: ( not LIN a,a1,d & not b,c // b1,c1 ) ; :: thesis: contradiction
A9: ( c <> c1 & a <> a1 & b <> b1 )

proof

assume A10: ( not c <> c1 or not a <> a1 or not b <> b1 ) ; :: thesis: contradiction

A11: now

assume A12: c = c1 ; :: thesis: contradiction
A13: not LIN o,c,a

proof

assume LIN o,c,a ; :: thesis: contradiction
then a in M by A7, AFF_1:39;
then A14: o,a // M by A7, AFF_1:66;
o,a // Y by A7, AFF_1:66;
then Y // M by A7, A14, AFF_1:67;
hence contradiction by A7, AFF_1:59; :: thesis: verum

end;

Y // Y by A7, AFF_1:55;
then o,a // o,a1 by A7, AFF_1:53;
then A15: LIN o,a,a1 by AFF_1:def 1;
c,a // c,a1 by A7, A12, AFF_1:13;
then A16: a = a1 by A13, A15, AFF_1:23;
A17: not LIN o,a,b

proof

assume LIN o,a,b ; :: thesis: contradiction
then b in Y by A7, AFF_1:39;
then A18: o,b // Y by A7, AFF_1:66;
o,b // Z by A7, AFF_1:66;
then Y // Z by A7, A18, AFF_1:67;
hence contradiction by A7, AFF_1:59; :: thesis: verum

end;

Z // Z by A7, AFF_1:55;
then o,b // o,b1 by A7, AFF_1:53;
then LIN o,b,b1 by AFF_1:def 1;
then b = b1 by A7, A16, A17, AFF_1:23;
hence contradiction by A8, A12, AFF_1:11; :: thesis: verum

end;

A19: now

assume A20: a = a1 ; :: thesis: contradiction
A21: not LIN o,a,b

proof

assume LIN o,a,b ; :: thesis: contradiction
then b in Y by A7, AFF_1:39;
then A22: o,b // Y by A7, AFF_1:66;
o,b // Z by A7, AFF_1:66;
then Y // Z by A7, A22, AFF_1:67;
hence contradiction by A7, AFF_1:59; :: thesis: verum

end;

Z // Z by A7, AFF_1:55;
then o,b // o,b1 by A7, AFF_1:53;
then LIN o,b,b1 by AFF_1:def 1;
then A23: b = b1 by A7, A20, A21, AFF_1:23;
A24: not LIN o,a,c

proof

assume LIN o,a,c ; :: thesis: contradiction
then c in Y by A7, AFF_1:39;
then A25: o,c // Y by A7, AFF_1:66;
o,c // M by A7, AFF_1:66;
then Y // M by A7, A25, AFF_1:67;
hence contradiction by A7, AFF_1:59; :: thesis: verum

end;

M // M by A7, AFF_1:55;
then o,c // o,c1 by A7, AFF_1:53;
then LIN o,c,c1 by AFF_1:def 1;
then c = c1 by A7, A20, A24, AFF_1:23;
hence contradiction by A8, A23, AFF_1:11; :: thesis: verum

end;

now

assume A26: b = b1 ; :: thesis: contradiction
A27: not LIN o,b,a

proof

assume LIN o,b,a ; :: thesis: contradiction
then a in Z by A7, AFF_1:39;
then A28: o,a // Z by A7, AFF_1:66;
o,a // Y by A7, AFF_1:66;
then Y // Z by A7, A28, AFF_1:67;
hence contradiction by A7, AFF_1:59; :: thesis: verum

end;

Y // Y by A7, AFF_1:55;
then o,a // o,a1 by A7, AFF_1:53;
then A29: LIN o,a,a1 by AFF_1:def 1;
b,a // b,a1 by A7, A26, AFF_1:13;
then A30: a = a1 by A27, A29, AFF_1:23;
A31: not LIN o,a,c

proof

assume LIN o,a,c ; :: thesis: contradiction
then c in Y by A7, AFF_1:39;
then A32: o,c // Y by A7, AFF_1:66;
o,c // M by A7, AFF_1:66;
then Y // M by A7, A32, AFF_1:67;
hence contradiction by A7, AFF_1:59; :: thesis: verum

end;

M // M by A7, AFF_1:55;
then o,c // o,c1 by A7, AFF_1:53;
then LIN o,c,c1 by AFF_1:def 1;
then c = c1 by A7, A30, A31, AFF_1:23;
hence contradiction by A8, A26, AFF_1:11; :: thesis: verum

end;

hence contradiction by A10, A11, A19; :: thesis: verum

end;

now

assume A33: b <> c ; :: thesis: contradiction

A34: now

assume A35: b1 = o ; :: thesis: contradiction
A36: o = a1

proof

assume A37: o <> a1 ; :: thesis: contradiction
A38: not LIN b,a,o

proof

assume LIN b,a,o ; :: thesis: contradiction
then LIN o,a,b by AFF_1:15;
then b in Y by A7, AFF_1:39;
then A39: o,b // Y by A7, AFF_1:66;
o,b // Z by A7, AFF_1:66;
then Y // Z by A7, A39, AFF_1:67;
hence contradiction by A7, AFF_1:59; :: thesis: verum

end;

A40: a,o // a,a1 by A7, AFF_1:65;
LIN b,o,a1

proof

a1,o // a,a1 by A7, AFF_1:65;
then a,b // a,a1 by A7, A35, A37, AFF_1:14;
then LIN a,b,a1 by AFF_1:def 1;
then LIN a1,b,a by AFF_1:15;
then A41: a1,b // a1,a by AFF_1:def 1;
A42: a1 <> a

proof

assume a1 = a ; :: thesis: contradiction
then LIN a,b,o by A7, A35, AFF_1:def 1;
then LIN o,a,b by AFF_1:15;
then b in Y by A7, AFF_1:39;
then A43: o,b // Y by A7, AFF_1:66;
o,b // Z by A7, AFF_1:66;
then Y // Z by A7, A43, AFF_1:67;
hence contradiction by A7, AFF_1:59; :: thesis: verum

end;

a1,a // a1,o by A7, AFF_1:65;
then a1,b // a1,o by A41, A42, AFF_1:14;
then LIN a1,b,o by AFF_1:def 1;
hence LIN b,o,a1 by AFF_1:15; :: thesis: verum

end;

hence contradiction by A37, A38, A40, AFF_1:23; :: thesis: verum

end;

o = c1

proof

assume A44: o <> c1 ; :: thesis: contradiction
A45: not LIN a,c,o

proof

assume LIN a,c,o ; :: thesis: contradiction
then LIN o,a,c by AFF_1:15;
then c in Y by A7, AFF_1:39;
then A46: o,c // Y by A7, AFF_1:66;
o,c // M by A7, AFF_1:66;
then Y // M by A7, A46, AFF_1:67;
hence contradiction by A7, AFF_1:59; :: thesis: verum

end;

A47: LIN a,o,c1

proof

A48: o,c1 // o,c by A7, AFF_1:65;
then o,c // a,c by A7, A36, A44, AFF_1:14;
then c,o // c,a by AFF_1:13;
then LIN c,o,a by AFF_1:def 1;
then LIN o,a,c by AFF_1:15;
then o,a // o,c by AFF_1:def 1;
then o,a // o,c1 by A7, A48, AFF_1:14;
then LIN o,a,c1 by AFF_1:def 1;
hence LIN a,o,c1 by AFF_1:15; :: thesis: verum

end;

c,o // c,c1 by A7, AFF_1:65;
hence contradiction by A44, A45, A47, AFF_1:23; :: thesis: verum

end;

hence contradiction by A8, A35, AFF_1:12; :: thesis: verum

end;

now

assume A49: b1 <> o ; :: thesis: contradiction
A50: ( a <> b & a <> c )

proof

assume A51: ( not a <> b or not a <> c ) ; :: thesis: contradiction

A52: now

assume a = b ; :: thesis: contradiction
then A53: o,a // Z by A7, AFF_1:66;
o,a // Y by A7, AFF_1:66;
then Y // Z by A7, A53, AFF_1:67;
hence contradiction by A7, AFF_1:59; :: thesis: verum

end;

now

assume a = c ; :: thesis: contradiction
then A54: o,a // M by A7, AFF_1:66;
o,a // Y by A7, AFF_1:66;
then Y // M by A7, A54, AFF_1:67;
hence contradiction by A7, AFF_1:59; :: thesis: verum

end;

hence contradiction by A51, A52; :: thesis: verum

end;

A55: ( a1 <> b1 & a1 <> c1 )

proof

assume A56: ( not a1 <> b1 or not a1 <> c1 ) ; :: thesis: contradiction

A57: now

assume a1 = b1 ; :: thesis: contradiction
then A58: o,b1 // Y by A7, AFF_1:66;
o,b1 // Z by A7, AFF_1:66;
then Y // Z by A49, A58, AFF_1:67;
hence contradiction by A7, AFF_1:59; :: thesis: verum

end;

now

assume a1 = c1 ; :: thesis: contradiction
then A59: o,a1 // M by A7, AFF_1:66;
A60: o <> a1

proof

assume A61: o = a1 ; :: thesis: contradiction
A62: not LIN a,b,o

proof

assume LIN a,b,o ; :: thesis: contradiction
then LIN o,a,b by AFF_1:15;
then b in Y by A7, AFF_1:39;
then A63: o,b // Y by A7, AFF_1:66;
o,b // Z by A7, AFF_1:66;
then Y // Z by A7, A63, AFF_1:67;
hence contradiction by A7, AFF_1:59; :: thesis: verum

end;

Z // Z by A7, AFF_1:55;
then A64: o,b // o,b1 by A7, AFF_1:53;
then a,b // o,b by A7, A49, A61, AFF_1:14;
then b,a // b,o by AFF_1:13;
then LIN b,a,o by AFF_1:def 1;
then LIN o,a,b by AFF_1:15;
then o,a // o,b by AFF_1:def 1;
then o,a // o,b1 by A7, A64, AFF_1:14;
then LIN o,a,b1 by AFF_1:def 1;
then A65: LIN a,o,b1 by AFF_1:15;
Z // Z by A7, AFF_1:55;
then b,o // b,b1 by A7, AFF_1:53;
hence contradiction by A49, A62, A65, AFF_1:23; :: thesis: verum

end;

o,a1 // Y by A7, AFF_1:66;
then Y // M by A59, A60, AFF_1:67;
hence contradiction by A7, AFF_1:59; :: thesis: verum

end;

hence contradiction by A56, A57; :: thesis: verum

end;

A66: ( b <> c & b1 <> c1 ) by A8, AFF_1:12;
LIN b,b,c by AFF_1:16;
then consider A being Subset of X such that
A67: ( A is being_line & b in A & b in A & c in A ) by AFF_1:33;
LIN b1,b1,c1 by AFF_1:16;
then consider K being Subset of X such that
A68: ( K is being_line & b1 in K & b1 in K & c1 in K ) by AFF_1:33;
LIN o,o,a by AFF_1:16;
then consider C being Subset of X such that
A69: ( C is being_line & o in C & o in C & a in C ) by AFF_1:33;
ex d1 being Element of X st
( d1 in C & c,c1 // d,d1 )

proof

consider e1 being Element of X such that
A70: ( o,a // o,e1 & o <> e1 ) by DIRAF:47;
consider e2 being Element of X such that
A71: ( c,c1 // d,e2 & d <> e2 ) by DIRAF:47;
not o,e1 // d,e2

proof

assume o,e1 // d,e2 ; :: thesis: contradiction
then o,a // d,e2 by A70, AFF_1:14;
then A72: o,a // c,c1 by A71, AFF_1:14;
M // M by A7, AFF_1:55;
then c,c1 // o,c by A7, AFF_1:53;
then o,a // o,c by A9, A72, AFF_1:14;
then LIN o,a,c by AFF_1:def 1;
then c in Y by A7, AFF_1:39;
then A73: o,c // Y by A7, AFF_1:66;
o,c // M by A7, AFF_1:66;
then Y // M by A7, A73, AFF_1:67;
hence contradiction by A7, AFF_1:59; :: thesis: verum

end;

then consider d1 being Element of X such that
A74: ( LIN o,e1,d1 & LIN d,e2,d1 ) by AFF_1:74;
take d1 ; :: thesis: ( d1 in C & c,c1 // d,d1 )
LIN o,a,e1 by A70, AFF_1:def 1;
then A75: e1 in C by A7, A69, AFF_1:39;
d,e2 // d,d1 by A74, AFF_1:def 1;
hence ( d1 in C & c,c1 // d,d1 ) by A69, A70, A71, A74, A75, AFF_1:14, AFF_1:39; :: thesis: verum

end;

then consider d1 being Element of X such that
A76: ( d1 in C & c,c1 // d,d1 ) ;
ex d2 being Element of X st
( d2 in C & a,c // d,d2 )

proof

consider e1 being Element of X such that
A77: ( o,a // o,e1 & o <> e1 ) by DIRAF:47;
consider e2 being Element of X such that
A78: ( a,c // d,e2 & d <> e2 ) by DIRAF:47;
not o,e1 // d,e2

proof

assume o,e1 // d,e2 ; :: thesis: contradiction
then o,a // d,e2 by A77, AFF_1:14;
then o,a // a,c by A78, AFF_1:14;
then a,o // a,c by AFF_1:13;
then LIN a,o,c by AFF_1:def 1;
then c in Y by A7, AFF_1:39;
then A79: o,c // Y by A7, AFF_1:66;
o,c // M by A7, AFF_1:66;
then Y // M by A7, A79, AFF_1:67;
hence contradiction by A7, AFF_1:59; :: thesis: verum

end;

then consider d2 being Element of X such that
A80: ( LIN o,e1,d2 & LIN d,e2,d2 ) by AFF_1:74;
take d2 ; :: thesis: ( d2 in C & a,c // d,d2 )
LIN o,a,e1 by A77, AFF_1:def 1;
then A81: e1 in C by A7, A69, AFF_1:39;
d,e2 // d,d2 by A80, AFF_1:def 1;
hence ( d2 in C & a,c // d,d2 ) by A69, A77, A78, A80, A81, AFF_1:14, AFF_1:39; :: thesis: verum

end;

then consider d2 being Element of X such that
A82: ( d2 in C & a,c // d,d2 ) ;
ex d3 being Element of X st
( d3 in A & o,b // d1,d3 )

proof

consider e1 being Element of X such that
A83: ( b,c // b,e1 & b <> e1 ) by DIRAF:47;
consider e2 being Element of X such that
A84: ( o,b // d1,e2 & d1 <> e2 ) by DIRAF:47;
not b,e1 // d1,e2

proof

assume b,e1 // d1,e2 ; :: thesis: contradiction
then b,c // d1,e2 by A83, AFF_1:14;
then A85: b,c // o,b by A84, AFF_1:14;
then b,c // b,o by AFF_1:13;
then LIN b,c,o by AFF_1:def 1;
then LIN o,b,c by AFF_1:15;
then A86: o,b // o,c by AFF_1:def 1;
A87: ( Z // Z & M // M ) by A7, AFF_1:55;
then A88: o,b // o,b1 by A7, AFF_1:53;
o,c // o,c1 by A7, A87, AFF_1:53;
then o,b // o,c1 by A7, A86, AFF_1:14;
then o,b1 // o,c1 by A7, A88, AFF_1:14;
then LIN o,b1,c1 by AFF_1:def 1;
then LIN b1,c1,o by AFF_1:15;
then b1,c1 // b1,o by AFF_1:def 1;
then b1,c1 // o,b1 by AFF_1:13;
then b1,c1 // o,b by A49, A88, AFF_1:14;
hence contradiction by A7, A8, A85, AFF_1:14; :: thesis: verum

end;

then consider d3 being Element of X such that
A89: ( LIN b,e1,d3 & LIN d1,e2,d3 ) by AFF_1:74;
take d3 ; :: thesis: ( d3 in A & o,b // d1,d3 )
LIN b,c,e1 by A83, AFF_1:def 1;
then A90: e1 in A by A66, A67, AFF_1:39;
d1,e2 // d1,d3 by A89, AFF_1:def 1;
hence ( d3 in A & o,b // d1,d3 ) by A67, A83, A84, A89, A90, AFF_1:14, AFF_1:39; :: thesis: verum

end;

then consider d3 being Element of X such that
A91: ( d3 in A & o,b // d1,d3 ) ;
ex d4 being Element of X st
( d4 in K & d1,d3 // d1,d4 )

proof

consider e1 being Element of X such that
A92: ( b1,c1 // b1,e1 & b1 <> e1 ) by DIRAF:47;
consider e2 being Element of X such that
A93: ( d1,d3 // d1,e2 & d1 <> e2 ) by DIRAF:47;
not b1,e1 // d1,e2

proof

assume b1,e1 // d1,e2 ; :: thesis: contradiction
then b1,c1 // d1,e2 by A92, AFF_1:14;
then A94: b1,c1 // d1,d3 by A93, AFF_1:14;
A95: d1 <> d3

proof

assume A96: d1 = d3 ; :: thesis: contradiction
A97: d <> d1

proof

assume A98: d = d1 ; :: thesis: contradiction
Y // Y by A7, AFF_1:55;
then o,a // o,a1 by A7, AFF_1:53;
then LIN o,a,a1 by AFF_1:def 1;
then A99: a1 in C by A7, A69, AFF_1:39;
C // C by A69, AFF_1:55;
then a,a1 // a,d by A69, A76, A98, A99, AFF_1:53;
hence contradiction by A8, AFF_1:def 1; :: thesis: verum

end;

A100: d in A by A7, A66, A67, AFF_1:39;
M // M by A7, AFF_1:55;
then c,c1 // o,c by A7, AFF_1:53;
then o,c // d,d1 by A9, A76, AFF_1:14;
then d,d1 // c,o by AFF_1:13;
then A101: o in A by A67, A91, A96, A97, A100, AFF_1:62;
A // A by A67, AFF_1:55;
then A102: o,b // o,c by A67, A101, AFF_1:53;
then LIN o,b,c by AFF_1:def 1;
then LIN b,c,o by AFF_1:15;
then b,c // b,o by AFF_1:def 1;
then A103: b,c // o,b by AFF_1:13;
A104: ( Z // Z & M // M ) by A7, AFF_1:55;
then A105: o,b // o,b1 by A7, AFF_1:53;
o,c // o,c1 by A7, A104, AFF_1:53;
then o,b // o,c1 by A7, A102, AFF_1:14;
then o,b1 // o,c1 by A7, A105, AFF_1:14;
then LIN o,b1,c1 by AFF_1:def 1;
then LIN b1,c1,o by AFF_1:15;
then b1,c1 // b1,o by AFF_1:def 1;
then b1,c1 // o,b1 by AFF_1:13;
then o,b // b1,c1 by A49, A105, AFF_1:14;
hence contradiction by A7, A8, A103, AFF_1:14; :: thesis: verum

end;

Z // Z by A7, AFF_1:55;
then A106: o,b // o,b1 by A7, AFF_1:53;
then o,b1 // d1,d3 by A7, A91, AFF_1:14;
then A107: o,b1 // b1,c1 by A94, A95, AFF_1:14;
then b1,o // b1,c1 by AFF_1:13;
then LIN b1,o,c1 by AFF_1:def 1;
then LIN o,b1,c1 by AFF_1:15;
then o,b1 // o,c1 by AFF_1:def 1;
then A108: o,b // o,c1 by A49, A106, AFF_1:14;
A109: o <> c1

proof

assume A110: o = c1 ; :: thesis: contradiction
A111: not LIN a,c,o

proof

assume LIN a,c,o ; :: thesis: contradiction
then LIN o,a,c by AFF_1:15;
then c in Y by A7, AFF_1:39;
then A112: o,c // Y by A7, AFF_1:66;
o,c // M by A7, AFF_1:66;
then Y // M by A7, A112, AFF_1:67;
hence contradiction by A7, AFF_1:59; :: thesis: verum

end;

Y // Y by A7, AFF_1:55;
then a,o // a,a1 by A7, AFF_1:53;
then A113: LIN a,o,a1 by AFF_1:def 1;
c,o // c,a1

proof

Y // Y by A7, AFF_1:55;
then a1,o // a,a1 by A7, AFF_1:53;
then a,c // a,a1 by A7, A55, A110, AFF_1:14;
then LIN a,c,a1 by AFF_1:def 1;
then LIN a1,c,a by AFF_1:15;
then A114: a1,c // a1,a by AFF_1:def 1;
Y // Y by A7, AFF_1:55;
then a1,a // a1,o by A7, AFF_1:53;
then a1,c // a1,o by A9, A114, AFF_1:14;
then LIN a1,c,o by AFF_1:def 1;
then LIN c,o,a1 by AFF_1:15;
hence c,o // c,a1 by AFF_1:def 1; :: thesis: verum

end;

hence contradiction by A55, A110, A111, A113, AFF_1:23; :: thesis: verum

end;

M // M by A7, AFF_1:55;
then o,c // o,c1 by A7, AFF_1:53;
then o,b // o,c by A108, A109, AFF_1:14;
then LIN o,b,c by AFF_1:def 1;
then LIN b,o,c by AFF_1:15;
then b,o // b,c by AFF_1:def 1;
then o,b // b,c by AFF_1:13;
then o,b1 // b,c by A7, A106, AFF_1:14;
hence contradiction by A8, A49, A107, AFF_1:14; :: thesis: verum

end;

then consider d4 being Element of X such that
A115: ( LIN b1,e1,d4 & LIN d1,e2,d4 ) by AFF_1:74;
take d4 ; :: thesis: ( d4 in K & d1,d3 // d1,d4 )
LIN b1,c1,e1 by A92, AFF_1:def 1;
then A116: e1 in K by A66, A68, AFF_1:39;
d1,e2 // d1,d4 by A115, AFF_1:def 1;
hence ( d4 in K & d1,d3 // d1,d4 ) by A68, A92, A93, A115, A116, AFF_1:14, AFF_1:39; :: thesis: verum

end;

then consider d4 being Element of X such that
A117: ( d4 in K & d1,d3 // d1,d4 ) ;
A118: ( c in A & b in A & d in A & d3 in A ) by A7, A33, A67, A91, AFF_1:39;
A119: ( not o in A & not a in A & not d1 in A & not d2 in A )

proof

assume A120: ( o in A or a in A or d1 in A or d2 in A ) ; :: thesis: contradiction

A121: now

assume A122: o in A ; :: thesis: contradiction
A // A by A67, AFF_1:55;
then A123: o,b // o,c by A67, A122, AFF_1:53;
then LIN o,b,c by AFF_1:def 1;
then LIN b,c,o by AFF_1:15;
then A124: b,c // b,o by AFF_1:def 1;
Z // Z by A7, AFF_1:55;
then A125: o,b // o,b1 by A7, AFF_1:53;
M // M by A7, AFF_1:55;
then o,c // o,c1 by A7, AFF_1:53;
then o,b // o,c1 by A7, A123, AFF_1:14;
then o,b1 // o,c1 by A7, A125, AFF_1:14;
then LIN o,b1,c1 by AFF_1:def 1;
then LIN b1,c1,o by AFF_1:15;
then b1,c1 // b1,o by AFF_1:def 1;
then b1,c1 // o,b1 by AFF_1:13;
then o,b // b1,c1 by A49, A125, AFF_1:14;
then b,o // b1,c1 by AFF_1:13;
hence contradiction by A7, A8, A124, AFF_1:14; :: thesis: verum

end;

A126: now

assume A127: a in A ; :: thesis: contradiction
A // A by A67, AFF_1:55;
then A128: a,b // a,c by A67, A127, AFF_1:53;
A129: a <> b

proof

assume a = b ; :: thesis: contradiction
then A130: o,b // Y by A7, AFF_1:66;
o,b // Z by A7, AFF_1:66;
then Y // Z by A7, A130, AFF_1:67;
hence contradiction by A7, AFF_1:59; :: thesis: verum

end;

a <> c

proof

assume a = c ; :: thesis: contradiction
then A131: o,c // Y by A7, AFF_1:66;
o,c // M by A7, AFF_1:66;
then Y // M by A7, A131, AFF_1:67;
hence contradiction by A7, AFF_1:59; :: thesis: verum

end;

then a,b // a1,c1 by A7, A128, AFF_1:14;
then a1,b1 // a1,c1 by A7, A129, AFF_1:14;
then LIN a1,b1,c1 by AFF_1:def 1;
then LIN b1,c1,a1 by AFF_1:15;
then b1,c1 // b1,a1 by AFF_1:def 1;
then A132: a1,b1 // b1,c1 by AFF_1:13;
A133: a1 <> b1

proof

assume a1 = b1 ; :: thesis: contradiction
then A134: o,b1 // Y by A7, AFF_1:66;
o,b1 // Z by A7, AFF_1:66;
then Y // Z by A49, A134, AFF_1:67;
hence contradiction by A7, AFF_1:59; :: thesis: verum

end;

LIN a,b,c by A128, 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 b,c // a1,b1 by A7, A129, AFF_1:14;
hence contradiction by A8, A132, A133, AFF_1:14; :: thesis: verum

end;

A135: now

assume A136: d1 in A ; :: thesis: contradiction
A137: d <> d1

proof

assume A138: d = d1 ; :: thesis: contradiction
Y // Y by A7, AFF_1:55;
then o,a // o,a1 by A7, AFF_1:53;
then LIN o,a,a1 by AFF_1:def 1;
then A139: a1 in C by A7, A69, AFF_1:39;
C // C by A69, AFF_1:55;
then a,a1 // a,d by A69, A76, A138, A139, AFF_1:53;
hence contradiction by A8, AFF_1:def 1; :: thesis: verum

end;

A140: d in A by A7, A66, A67, AFF_1:39;
d,d1 // c,c1 by A76, AFF_1:13;
then A141: c1 in A by A67, A136, A137, A140, AFF_1:62;
M // M by A7, AFF_1:55;
then c,c1 // c,o by A7, AFF_1:53;
then LIN c,c1,o by AFF_1:def 1;
hence contradiction by A9, A67, A121, A141, AFF_1:39; :: thesis: verum

end;

now

assume A142: d2 in A ; :: thesis: contradiction
A143: d <> d2

proof

assume A144: d = d2 ; :: thesis: contradiction
Y // Y by A7, AFF_1:55;
then o,a // o,a1 by A7, AFF_1:53;
then LIN o,a,a1 by AFF_1:def 1;
then A145: a1 in C by A7, A69, AFF_1:39;
C // C by A69, AFF_1:55;
then a,a1 // a,d by A69, A82, A144, A145, AFF_1:53;
hence contradiction by A8, AFF_1:def 1; :: thesis: verum

end;

A146: d in A by A7, A66, A67, AFF_1:39;
d,d2 // c,a by A82, AFF_1:13;
hence contradiction by A67, A126, A142, A143, A146, AFF_1:62; :: thesis: verum

end;

hence contradiction by A120, A121, A126, A135; :: thesis: verum

end;

A147: ( not c in C & not b in C & not d in C & not d3 in C )

proof

assume A148: ( c in C or b in C or d in C or d3 in C ) ; :: thesis: contradiction

A149: now

assume A150: c in C ; :: thesis: contradiction
C // C by A69, AFF_1:55;
then o,a // o,c by A69, A150, AFF_1:53;
then LIN o,a,c by AFF_1:def 1;
then c in Y by A7, AFF_1:39;
then A151: o,c // Y by A7, AFF_1:66;
o,c // M by A7, AFF_1:66;
then Y // M by A7, A151, AFF_1:67;
hence contradiction by A7, AFF_1:59; :: thesis: verum

end;

A152: now

assume A153: b in C ; :: thesis: contradiction
C // C by A69, AFF_1:55;
then o,a // o,b by A69, A153, AFF_1:53;
then LIN o,a,b by AFF_1:def 1;
then b in Y by A7, AFF_1:39;
then A154: o,b // Y by A7, AFF_1:66;
o,b // Z by A7, AFF_1:66;
then Y // Z by A7, A154, AFF_1:67;
hence contradiction by A7, AFF_1:59; :: thesis: verum

end;

A155: now

assume A156: d in C ; :: thesis: contradiction
C // C by A69, AFF_1:55;
then A157: o,a // a,d by A69, A156, AFF_1:53;
Y // Y by A7, AFF_1:55;
then o,a // a,a1 by A7, AFF_1:53;
then a,a1 // a,d by A7, A157, AFF_1:14;
hence contradiction by A8, AFF_1:def 1; :: thesis: verum

end;

now

assume A158: d3 in C ; :: thesis: contradiction
A159: d1 <> d3

proof

assume A160: d1 = d3 ; :: thesis: contradiction
A161: d <> d1

proof

assume A162: d = d1 ; :: thesis: contradiction
Y // Y by A7, AFF_1:55;
then o,a // o,a1 by A7, AFF_1:53;
then LIN o,a,a1 by AFF_1:def 1;
then A163: a1 in C by A7, A69, AFF_1:39;
C // C by A69, AFF_1:55;
then a,a1 // a,d by A69, A76, A162, A163, AFF_1:53;
hence contradiction by A8, AFF_1:def 1; :: thesis: verum

end;

A164: d in A by A7, A66, A67, AFF_1:39;
d,d1 // c,c1 by A76, AFF_1:13;
then A165: c1 in A by A67, A91, A160, A161, A164, AFF_1:62;
A // A by A67, AFF_1:55;
then A166: c,c1 // c,b by A67, A165, AFF_1:53;
M // M by A7, AFF_1:55;
then c,o // c,c1 by A7, AFF_1:53;
then c,o // c,b by A9, A166, AFF_1:14;
then A167: LIN c,o,b by AFF_1:def 1;
then LIN o,b,c by AFF_1:15;
then A168: o,b // o,c by AFF_1:def 1;
( M // M & Z // Z ) by A7, AFF_1:55;
then A169: ( o,b // o,b1 & o,c // o,c1 ) by A7, AFF_1:53;
then o,b1 // o,c by A7, A168, AFF_1:14;
then o,b1 // o,c1 by A7, A169, AFF_1:14;
then LIN o,b1,c1 by AFF_1:def 1;
then LIN b1,c1,o by AFF_1:15;
then b1,c1 // b1,o by AFF_1:def 1;
then b1,c1 // o,b1 by AFF_1:13;
then A170: o,b // b1,c1 by A49, A169, AFF_1:14;
LIN b,c,o by A167, AFF_1:15;
then b,c // b,o by AFF_1:def 1;
then b,c // o,b by AFF_1:13;
hence contradiction by A7, A8, A170, AFF_1:14; :: thesis: verum

end;

d1,d3 // o,b by A91, AFF_1:13;
hence contradiction by A69, A76, A152, A158, A159, AFF_1:62; :: thesis: verum

end;

hence contradiction by A148, A149, A152, A155; :: thesis: verum

end;

A171: a,c // d2,d by A82, AFF_1:13;
c,o // d,d1

proof

M // M by A7, AFF_1:55;
then c,c1 // c,o by A7, AFF_1:53;
hence c,o // d,d1 by A9, A76, AFF_1:14; :: thesis: verum

end;

then A172: a,b // d2,d3 by A6, A67, A69, A76, A82, A91, A118, A119, A147, A171, Def3;
A173: ( o in C & a1 in C & d1 in C & d2 in C )

proof

a1 in C

proof

Y // Y by A7, AFF_1:55;
then o,a // o,a1 by A7, AFF_1:53;
then LIN o,a,a1 by AFF_1:def 1;
hence a1 in C by A7, A69, AFF_1:39; :: thesis: verum

end;

hence ( o in C & a1 in C & d1 in C & d2 in C ) by A69, A76, A82; :: thesis: verum

end;

A174: ( c1 in K & b1 in K & d in K & d4 in K )

proof

d in K

proof

b1 <> c1 by A8, AFF_1:12;
hence d in K by A7, A68, AFF_1:39; :: thesis: verum

end;

hence ( c1 in K & b1 in K & d in K & d4 in K ) by A68, A117; :: thesis: verum

end;

A175: ( not o in K & not a1 in K & not d1 in K & not d2 in K )

proof

assume A176: ( o in K or a1 in K or d1 in K or d2 in K ) ; :: thesis: contradiction

A177: now

assume A178: o in K ; :: thesis: contradiction
K // K by A68, AFF_1:55;
then A179: o,b1 // o,c1 by A68, A178, AFF_1:53;
then LIN o,b1,c1 by AFF_1:def 1;
then LIN b1,c1,o by AFF_1:15;
then A180: b1,c1 // b1,o by AFF_1:def 1;
Z // Z by A7, AFF_1:55;
then A181: o,b1 // o,b by A7, AFF_1:53;
then A182: o,b // o,c1 by A49, A179, AFF_1:14;
A183: o <> c1

proof

assume A184: o = c1 ; :: thesis: contradiction
A185: a1 <> o

proof

assume A186: a1 = o ; :: thesis: contradiction
A187: not LIN a,b,o

proof

assume LIN a,b,o ; :: thesis: contradiction
then LIN o,a,b by AFF_1:15;
then b in Y by A7, AFF_1:39;
then A188: o,b // Y by A7, AFF_1:66;
o,b // Z by A7, AFF_1:66;
then Y // Z by A7, A188, AFF_1:67;
hence contradiction by A7, AFF_1:59; :: thesis: verum

end;

Z // Z by A7, AFF_1:55;
then A189: o,b // o,b1 by A7, AFF_1:53;
then a,b // o,b by A7, A49, A186, AFF_1:14;
then b,a // b,o by AFF_1:13;
then LIN b,a,o by AFF_1:def 1;
then LIN o,a,b by AFF_1:15;
then o,a // o,b by AFF_1:def 1;
then o,a // o,b1 by A7, A189, AFF_1:14;
then LIN o,a,b1 by AFF_1:def 1;
then A190: LIN a,o,b1 by AFF_1:15;
Z // Z by A7, AFF_1:55;
then b,o // b,b1 by A7, AFF_1:53;
hence contradiction by A49, A187, A190, AFF_1:23; :: thesis: verum

end;

A191: not LIN c,a,o

proof

assume LIN c,a,o ; :: thesis: contradiction
then LIN o,a,c by AFF_1:15;
then c in Y by A7, AFF_1:39;
then A192: o,c // Y by A7, AFF_1:66;
o,c // M by A7, AFF_1:66;
then Y // M by A7, A192, AFF_1:67;
hence contradiction by A7, AFF_1:59; :: thesis: verum

end;

A193: LIN c,o,a1

proof

Y // Y by A7, AFF_1:55;
then A194: a1,o // o,a by A7, AFF_1:53;
then a,c // o,a by A7, A184, A185, AFF_1:14;
then a,c // a,o by AFF_1:13;
then LIN a,c,o by AFF_1:def 1;
then LIN o,c,a by AFF_1:15;
then o,c // o,a by AFF_1:def 1;
then o,c // a1,o by A7, A194, AFF_1:14;
then o,c // o,a1 by AFF_1:13;
then LIN o,c,a1 by AFF_1:def 1;
hence LIN c,o,a1 by AFF_1:15; :: thesis: verum

end;

Y // Y by A7, AFF_1:55;
then a,o // a,a1 by A7, AFF_1:53;
hence contradiction by A185, A191, A193, AFF_1:23; :: thesis: verum

end;

M // M by A7, AFF_1:55;
then o,c // o,c1 by A7, AFF_1:53;
then o,b // o,c by A182, A183, AFF_1:14;
then LIN o,b,c by AFF_1:def 1;
then LIN b,c,o by AFF_1:15;
then b,c // b,o by AFF_1:def 1;
then b,c // o,b by AFF_1:13;
then b,c // o,b1 by A7, A181, AFF_1:14;
then b,c // b1,o by AFF_1:13;
hence contradiction by A8, A49, A180, AFF_1:14; :: thesis: verum

end;

A195: now

assume A196: a1 in K ; :: thesis: contradiction
K // K by A68, AFF_1:55;
then A197: a1,b1 // a1,c1 by A68, A196, AFF_1:53;
then LIN a1,b1,c1 by AFF_1:def 1;
then LIN b1,c1,a1 by AFF_1:15;
then b1,c1 // b1,a1 by AFF_1:def 1;
then A198: b1,c1 // a1,b1 by AFF_1:13;
a,b // a1,c1 by A7, A55, A197, AFF_1:14;
then a,b // a,c by A7, A55, 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 b,c // a1,b1 by A7, A50, AFF_1:14;
hence contradiction by A8, A55, A198, AFF_1:14; :: thesis: verum

end;

A199: now

assume A200: d1 in K ; :: thesis: contradiction
A201: d in K by A7, A66, A68, AFF_1:39;
A202: d <> d1

proof

assume A203: d = d1 ; :: thesis: contradiction
C // C by A69, AFF_1:55;
then A204: o,a // a,d by A69, A76, A203, AFF_1:53;
Y // Y by A7, AFF_1:55;
then o,a // a,a1 by A7, AFF_1:53;
then a,a1 // a,d by A7, A204, AFF_1:14;
hence contradiction by A8, AFF_1:def 1; :: thesis: verum

end;

d,d1 // c1,c by A76, AFF_1:13;
then A205: c in K by A68, A200, A201, A202, AFF_1:62;
M // M by A7, AFF_1:55;
then c,c1 // c,o by A7, AFF_1:53;
then LIN c,c1,o by AFF_1:def 1;
hence contradiction by A9, A68, A177, A205, AFF_1:39; :: thesis: verum

end;

now

assume A206: d2 in K ; :: thesis: contradiction
A207: d in K by A7, A66, A68, AFF_1:39;
A208: d <> d2

proof

assume A209: d = d2 ; :: thesis: contradiction
Y // Y by A7, AFF_1:55;
then A210: o,a // a,a1 by A7, AFF_1:53;
C // C by A69, AFF_1:55;
then o,a // a,d by A69, A82, A209, AFF_1:53;
then a,a1 // a,d by A7, A210, AFF_1:14;
hence contradiction by A8, AFF_1:def 1; :: thesis: verum

end;

d,d2 // a1,c1 by A7, A50, A82, AFF_1:14;
then d,d2 // c1,a1 by AFF_1:13;
hence contradiction by A68, A195, A206, A207, A208, AFF_1:62; :: thesis: verum

end;

hence contradiction by A176, A177, A195, A199; :: thesis: verum

end;

A211: ( not c1 in C & not b1 in C & not d in C & not d4 in C )

proof

assume A212: ( c1 in C or b1 in C or d in C or d4 in C ) ; :: thesis: contradiction

A213: now

assume A214: c1 in C ; :: thesis: contradiction
M // M by A7, AFF_1:55;
then o,c1 // c1,c by A7, AFF_1:53;
hence contradiction by A68, A69, A147, A175, A214, AFF_1:62; :: thesis: verum

end;

A215: now

assume A216: b1 in C ; :: thesis: contradiction
Z // Z by A7, AFF_1:55;
then o,b1 // o,b by A7, AFF_1:53;
hence contradiction by A49, A69, A147, A216, AFF_1:62; :: thesis: verum

end;

now

assume A217: d4 in C ; :: thesis: contradiction
d1,d4 // d1,d3 by A117, AFF_1:13;
hence contradiction by A69, A76, A117, A147, A175, A217, AFF_1:62; :: thesis: verum

end;

hence contradiction by A147, A212, A213, A215; :: thesis: verum

end;

A218: a1,c1 // d2,d

proof

a <> c

proof

assume A219: a = c ; :: thesis: contradiction
A220: o,a // Y by A7, AFF_1:66;
o,a // M by A7, A219, AFF_1:66;
then Y // M by A7, A220, AFF_1:67;
hence contradiction by A7, AFF_1:59; :: thesis: verum

end;

then a1,c1 // d,d2 by A7, A82, AFF_1:14;
hence a1,c1 // d2,d by AFF_1:13; :: thesis: verum

end;

A221: c1,o // d,d1

proof

M // M by A7, AFF_1:55;
then c1,o // c,c1 by A7, AFF_1:53;
hence c1,o // d,d1 by A9, A76, AFF_1:14; :: thesis: verum

end;

o,b1 // d1,d4

proof

A222: o,b // o,b1 by A7, AFF_1:65;
o,b // d1,d4 by A76, A91, A117, A147, AFF_1:14;
hence o,b1 // d1,d4 by A7, A222, AFF_1:14; :: thesis: verum

end;

then A223: a1,b1 // d2,d4 by A6, A68, A69, A173, A174, A175, A211, A218, A221, Def3;
A224: d1 <> d2

proof

assume d1 = d2 ; :: thesis: contradiction
then a,c // c,c1 by A76, A82, A147, AFF_1:14;
then c,c1 // c,a by AFF_1:13;
then LIN c,c1,a by AFF_1:def 1;
then a in M by A7, A9, AFF_1:39;
then A225: o,a // M by A7, AFF_1:66;
o,a // Y by A7, AFF_1:66;
then Y // M by A7, A225, AFF_1:67;
hence contradiction by A7, AFF_1:59; :: thesis: verum

end;

A226: d4 <> d3

proof

assume A227: d4 = d3 ; :: thesis: contradiction
d = d3

proof

assume A228: d <> d3 ; :: thesis: contradiction
A229: ( d in A & d in K ) by A7, A66, A67, A68, AFF_1:39;
A230: ( A // A & K // K ) by A67, A68, AFF_1:55;
then A231: b1,c1 // d,d3 by A68, A117, A227, A229, AFF_1:53;
b,c // d,d3 by A67, A91, A229, A230, AFF_1:53;
hence contradiction by A8, A228, A231, AFF_1:14; :: thesis: verum

end;

then A232: o,b // d,d1 by A91, AFF_1:13;
A233: ( M // M & Z // Z ) by A7, AFF_1:55;
then o,c // c,c1 by A7, AFF_1:53;
then o,c // d,d1 by A9, A76, AFF_1:14;
then A234: o,b // o,c by A76, A147, A232, AFF_1:14;
then LIN o,b,c by AFF_1:def 1;
then LIN b,c,o by AFF_1:15;
then b,c // b,o by AFF_1:def 1;
then A235: b,c // o,b by AFF_1:13;
A236: ( o,b // o,b1 & o,c // o,c1 ) by A7, A233, AFF_1:53;
then o,b1 // o,c by A7, A234, AFF_1:14;
then o,b1 // o,c1 by A7, A236, AFF_1:14;
then LIN o,b1,c1 by AFF_1:def 1;
then LIN b1,c1,o by AFF_1:15;
then b1,c1 // b1,o by AFF_1:def 1;
then b1,c1 // o,b1 by AFF_1:13;
then o,b // b1,c1 by A49, A236, AFF_1:14;
hence contradiction by A7, A8, A235, AFF_1:14; :: thesis: verum

end;

d2,d3 // a1,b1 by A7, A50, A172, AFF_1:14;
then d2,d3 // d2,d4 by A55, A223, AFF_1:14;
then LIN d2,d3,d4 by AFF_1:def 1;
then LIN d4,d3,d2 by AFF_1:15;
then A237: d4,d3 // d4,d2 by AFF_1:def 1;
LIN d1,d3,d4 by A117, AFF_1:def 1;
then LIN d4,d3,d1 by AFF_1:15;
then d4,d3 // d4,d1 by AFF_1:def 1;
then A238: d4,d2 // d4,d1 by A226, A237, AFF_1:14;
not LIN d4,d2,d1

proof

assume LIN d4,d2,d1 ; :: thesis: contradiction
then LIN d1,d2,d4 by AFF_1:15;
hence contradiction by A69, A76, A82, A211, A224, AFF_1:39; :: thesis: verum

end;

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

end;

hence contradiction by A34; :: thesis: verum

end;

hence contradiction by A8, AFF_1:12; :: thesis: verum

end;

hence ( LIN a,a1,d or b,c // b1,c1 ) ; :: thesis: verum

end;

A239: now

assume Z // M ; :: thesis: contradiction
then A240: ( b in M & b1 in M ) by A3, AFF_1:59;
M // M by A3, AFF_1:55;
hence contradiction by A3, A4, A240, AFF_1:53; :: thesis: verum

end;

now

assume A241: not Z // M ; :: thesis: contradiction
A242: ( Y // Y & Z // Z & M // M ) by A3, AFF_1:55;
A243: ( not a in Z & not a in M )

proof

assume A244: ( a in Z or a in M ) ; :: thesis: contradiction

A245: now

assume a in Z ; :: thesis: contradiction
then A246: o,a // Z by A3, AFF_1:66;
o,a // Y by A3, AFF_1:66;
then Y // Z by A3, A246, AFF_1:67;
hence contradiction by A3, AFF_1:59; :: thesis: verum

end;

now

assume a in M ; :: thesis: contradiction
then A247: o,a // M by A3, AFF_1:66;
o,a // Y by A3, AFF_1:66;
then Y // M by A3, A247, AFF_1:67;
hence contradiction by A3, AFF_1:59; :: thesis: verum

end;

hence contradiction by A244, A245; :: thesis: verum

end;

A248: ( a <> a1 & b <> b1 & c <> c1 )

proof

assume A249: ( not a <> a1 or not b <> b1 or not c <> c1 ) ; :: thesis: contradiction

A250: now

assume A251: a = a1 ; :: thesis: contradiction
A252: not LIN a,o,b

proof

assume LIN a,o,b ; :: thesis: contradiction
then LIN o,b,a by AFF_1:15;
hence contradiction by A3, A243, AFF_1:39; :: thesis: verum

end;

A253: LIN a,b,b1 by A3, A251, AFF_1:def 1;
o,b // o,b1 by A3, A242, AFF_1:53;
then A254: b = b1 by A252, A253, AFF_1:23;
A255: not LIN a,o,c

proof

assume LIN a,o,c ; :: thesis: contradiction
then LIN o,c,a by AFF_1:15;
hence contradiction by A3, A243, AFF_1:39; :: thesis: verum

end;

A256: LIN a,c,c1 by A3, A251, AFF_1:def 1;
o,c // o,c1 by A3, A242, AFF_1:53;
then c = c1 by A255, A256, AFF_1:23;
hence contradiction by A4, A254, AFF_1:11; :: thesis: verum

end;

A257: now

assume A258: b = b1 ; :: thesis: contradiction
A259: not LIN b,o,a by A3, A243, AFF_1:39;
b,a // b,a1 by A3, A258, AFF_1:13;
then A260: LIN b,a,a1 by AFF_1:def 1;
o,a // o,a1 by A3, A242, AFF_1:53;
hence contradiction by A250, A259, A260, AFF_1:23; :: thesis: verum

end;

now

assume A261: c = c1 ; :: thesis: contradiction
A262: not LIN c,o,a by A3, A243, AFF_1:39;
c,a // c,a1 by A3, A261, AFF_1:13;
then A263: LIN c,a,a1 by AFF_1:def 1;
o,a // o,a1 by A3, A242, AFF_1:53;
hence contradiction by A250, A262, A263, AFF_1:23; :: thesis: verum

end;

hence contradiction by A249, A250, A257; :: thesis: verum

end;

A264: ( a1 <> o & b1 <> o & c1 <> o )

proof

assume A265: ( not a1 <> o or not b1 <> o or not c1 <> o ) ; :: thesis: contradiction

A266: now

assume A267: a1 = o ; :: thesis: contradiction
A268: o = b1

proof

assume A269: o <> b1 ; :: thesis: contradiction
A270: not LIN b,a,o

proof

assume LIN b,a,o ; :: thesis: contradiction
then LIN o,b,a by AFF_1:15;
hence contradiction by A3, A243, AFF_1:39; :: thesis: verum

end;

b,o // b,b1 by A3, A242, AFF_1:53;
then A271: LIN b,o,b1 by AFF_1:def 1;
a,o // a,b1

proof

A272: o,b1 // o,b by A3, A242, AFF_1:53;
then a,b // o,b by A3, A267, A269, AFF_1:14;
then b,a // b,o by AFF_1:13;
then LIN b,a,o by AFF_1:def 1;
then LIN o,a,b by AFF_1:15;
then o,a // o,b by AFF_1:def 1;
then o,a // o,b1 by A3, A272, AFF_1:14;
then LIN o,a,b1 by AFF_1:def 1;
then LIN a,o,b1 by AFF_1:15;
hence a,o // a,b1 by AFF_1:def 1; :: thesis: verum

end;

hence contradiction by A269, A270, A271, AFF_1:23; :: thesis: verum

end;

o = c1

proof

assume A273: o <> c1 ; :: thesis: contradiction
A274: not LIN c,a,o

proof

assume LIN c,a,o ; :: thesis: contradiction
then LIN o,c,a by AFF_1:15;
hence contradiction by A3, A243, AFF_1:39; :: thesis: verum

end;

c,o // c,c1 by A3, A242, AFF_1:53;
then A275: LIN c,o,c1 by AFF_1:def 1;
a,o // a,c1

proof

A276: o,c1 // o,c by A3, A242, AFF_1:53;
then a,c // o,c by A3, A267, A273, AFF_1:14;
then c,o // c,a by AFF_1:13;
then LIN c,o,a by AFF_1:def 1;
then LIN o,c,a by AFF_1:15;
then o,c // o,a by AFF_1:def 1;
then o,c1 // o,a by A3, A276, AFF_1:14;
then LIN o,c1,a by AFF_1:def 1;
then LIN a,o,c1 by AFF_1:15;
hence a,o // a,c1 by AFF_1:def 1; :: thesis: verum

end;

hence contradiction by A273, A274, A275, AFF_1:23; :: thesis: verum

end;

hence contradiction by A4, A268, AFF_1:12; :: thesis: verum

end;

A277: now

assume A278: b1 = o ; :: thesis: contradiction
A279: not LIN a,b,o

proof

assume LIN a,b,o ; :: thesis: contradiction
then LIN o,b,a by AFF_1:15;
hence contradiction by A3, A243, AFF_1:39; :: thesis: verum

end;

a,o // a,a1 by A3, A242, AFF_1:53;
then A280: LIN a,o,a1 by AFF_1:def 1;
b,o // b,a1

proof

A281: a1,o // a,a1 by A3, A242, AFF_1:53;
then a,b // a,a1 by A3, A266, A278, AFF_1:14;
then LIN a,b,a1 by AFF_1:def 1;
then LIN a1,b,a by AFF_1:15;
then a1,b // a1,a by AFF_1:def 1;
then a1,b // a,a1 by AFF_1:13;
then a1,b // a1,o by A248, A281, AFF_1:14;
then LIN a1,b,o by AFF_1:def 1;
then LIN b,o,a1 by AFF_1:15;
hence b,o // b,a1 by AFF_1:def 1; :: thesis: verum

end;

hence contradiction by A266, A279, A280, AFF_1:23; :: thesis: verum

end;

now

assume A282: c1 = o ; :: thesis: contradiction
A283: not LIN a,c,o

proof

assume LIN a,c,o ; :: thesis: contradiction
then LIN o,c,a by AFF_1:15;
hence contradiction by A3, A243, AFF_1:39; :: thesis: verum

end;

a,o // a,a1 by A3, A242, AFF_1:53;
then A284: LIN a,o,a1 by AFF_1:def 1;
c,o // c,a1

proof

A285: a1,o // a,a1 by A3, A242, AFF_1:53;
then a,c // a,a1 by A3, A266, A282, AFF_1:14;
then LIN a,c,a1 by AFF_1:def 1;
then LIN a1,a,c by AFF_1:15;
then a1,a // a1,c by AFF_1:def 1;
then a,a1 // a1,c by AFF_1:13;
then a1,o // a1,c by A248, A285, AFF_1:14;
then LIN a1,o,c by AFF_1:def 1;
then LIN c,o,a1 by AFF_1:15;
hence c,o // c,a1 by AFF_1:def 1; :: thesis: verum

end;

hence contradiction by A266, A283, A284, AFF_1:23; :: thesis: verum

end;

hence contradiction by A265, A266, A277; :: thesis: verum

end;

consider d being Element of X such that
A286: ( LIN b,c,d & LIN b1,c1,d ) by A4, AFF_1:74;
A287: LIN a,a1,d by A2, A3, A4, A5, A286;
ex d1 being Element of X st
( a,b // d,d1 & d1 in Z )

proof

consider e1 being Element of X such that
A288: ( o,b // o,e1 & o <> e1 ) by DIRAF:47;
consider e2 being Element of X such that
A289: ( a,b // d,e2 & d <> e2 ) by DIRAF:47;
not o,e1 // d,e2

proof

assume o,e1 // d,e2 ; :: thesis: contradiction
then o,b // d,e2 by A288, AFF_1:14;
then o,b // a,b by A289, AFF_1:14;
then b,o // b,a by AFF_1:13;
then LIN b,o,a by AFF_1:def 1;
hence contradiction by A3, A243, AFF_1:39; :: thesis: verum

end;

then consider d1 being Element of X such that
A290: ( LIN o,e1,d1 & LIN d,e2,d1 ) by AFF_1:74;
take d1 ; :: thesis: ( a,b // d,d1 & d1 in Z )
o,e1 // o,d1 by A290, AFF_1:def 1;
then o,b // o,d1 by A288, AFF_1:14;
then A291: LIN o,b,d1 by AFF_1:def 1;
d,e2 // d,d1 by A290, AFF_1:def 1;
hence ( a,b // d,d1 & d1 in Z ) by A3, A289, A291, AFF_1:14, AFF_1:39; :: thesis: verum

end;

then consider d1 being Element of X such that
A292: ( a,b // d,d1 & d1 in Z ) ;
ex d2 being Element of X st
( a,c // d,d2 & d2 in M )

proof

consider e1 being Element of X such that
A293: ( o,c // o,e1 & o <> e1 ) by DIRAF:47;
consider e2 being Element of X such that
A294: ( a,c // d,e2 & d <> e2 ) by DIRAF:47;
not o,e1 // d,e2

proof

assume o,e1 // d,e2 ; :: thesis: contradiction
then o,c // d,e2 by A293, AFF_1:14;
then o,c // a,c by A294, AFF_1:14;
then c,o // c,a by AFF_1:13;
then LIN c,o,a by AFF_1:def 1;
hence contradiction by A3, A243, AFF_1:39; :: thesis: verum

end;

then consider d2 being Element of X such that
A295: ( LIN o,e1,d2 & LIN d,e2,d2 ) by AFF_1:74;
take d2 ; :: thesis: ( a,c // d,d2 & d2 in M )
o,e1 // o,d2 by A295, AFF_1:def 1;
then o,c // o,d2 by A293, AFF_1:14;
then A296: LIN o,c,d2 by AFF_1:def 1;
d,e2 // d,d2 by A295, AFF_1:def 1;
hence ( a,c // d,d2 & d2 in M ) by A3, A294, A296, AFF_1:14, AFF_1:39; :: thesis: verum

end;

then consider d2 being Element of X such that
A297: ( a,c // d,d2 & d2 in M ) ;
A298: d1 <> d2

proof

assume d1 = d2 ; :: thesis: contradiction
then A299: o,d1 // M by A3, A297, AFF_1:66;
A300: o <> d1

proof

assume A301: o = d1 ; :: thesis: contradiction
A302: a,a1 // a,d by A287, AFF_1:def 1;
A303: o <> d

proof

assume o = d ; :: thesis: contradiction
then LIN o,b,c by A286, AFF_1:15;
then c in Z by A3, AFF_1:39;
then A304: o,c // Z by A3, AFF_1:66;
o,c // M by A3, AFF_1:66;
hence contradiction by A3, A241, A304, AFF_1:67; :: thesis: verum

end;

a,o // a,a1 by A3, A242, AFF_1:53;
then a,o // a,d by A248, A302, AFF_1:14;
then LIN a,o,d by AFF_1:def 1;
then LIN o,a,d by AFF_1:15;
then o,a // o,d by AFF_1:def 1;
then a,o // d,o by AFF_1:13;
then a,b // a,o by A292, A301, A303, AFF_1:14;
then LIN a,b,o by AFF_1:def 1;
then LIN o,b,a by AFF_1:15;
hence contradiction by A3, A243, AFF_1:39; :: thesis: verum

end;

o,d1 // Z by A3, A292, AFF_1:66;
hence contradiction by A241, A299, A300, AFF_1:67; :: thesis: verum

end;

A305: now

assume A306: b1,c1 // d1,d2 ; :: thesis: contradiction
ex d5 being Element of X st
( LIN b,c,d5 & LIN d1,d2,d5 )

proof

consider e1 being Element of X such that
A307: ( b,c // b,e1 & b <> e1 ) by DIRAF:47;
consider e2 being Element of X such that
A308: ( d1,d2 // d1,e2 & d1 <> e2 ) by DIRAF:47;
not b,e1 // d1,e2

proof

assume b,e1 // d1,e2 ; :: thesis: contradiction
then b,e1 // d1,d2 by A308, AFF_1:14;
then b,c // d1,d2 by A307, AFF_1:14;
hence contradiction by A4, A298, A306, AFF_1:14; :: thesis: verum

end;

then consider d5 being Element of X such that
A309: ( LIN b,e1,d5 & LIN d1,e2,d5 ) by AFF_1:74;
take d5 ; :: thesis: ( LIN b,c,d5 & LIN d1,d2,d5 )
( d1,e2 // d1,d5 & b,e1 // b,d5 ) by A309, AFF_1:def 1;
then ( d1,d2 // d1,d5 & b,c // b,d5 ) by A307, A308, AFF_1:14;
hence ( LIN b,c,d5 & LIN d1,d2,d5 ) by AFF_1:def 1; :: thesis: verum

end;

then consider d5 being Element of X such that
A310: ( LIN b,c,d5 & LIN d1,d2,d5 ) ;
A311: d in Y by A3, A248, A287, AFF_1:39;

A312: now

assume A313: LIN a,d,d5 ; :: thesis: contradiction
A314: not LIN a,b,d

proof

assume LIN a,b,d ; :: thesis: contradiction
then A315: LIN a,d,b by AFF_1:15;
a <> d

proof

assume A316: a = d ; :: thesis: contradiction
then LIN a,b,c by A286, AFF_1:15;
then a,b // a,c by AFF_1:def 1;
then a1,b1 // a,c by A3, A243, AFF_1:14;
then a1,b1 // a1,c1 by A3, A243, AFF_1:14;
then LIN a1,b1,c1 by AFF_1:def 1;
then LIN b1,c1,a1 by AFF_1:15;
then b1,c1 // b1,a1 by AFF_1:def 1;
then A317: b1,c1 // a1,b1 by AFF_1:13;
A318: a1 <> b1

proof

assume A319: a1 = b1 ; :: thesis: contradiction
o,a1 // o,a by A3, A242, AFF_1:53;
then LIN o,a1,a by AFF_1:def 1;
hence contradiction by A3, A243, A264, A319, AFF_1:39; :: thesis: verum

end;

b,c // b,a by A286, A316, AFF_1:def 1;
then b,c // a,b by AFF_1:13;
then b,c // a1,b1 by A3, A243, AFF_1:14;
hence contradiction by A4, A317, A318, AFF_1:14; :: thesis: verum

end;

then b in Y by A3, A311, A315, AFF_1:39;
then A320: o,b // Y by A3, AFF_1:66;
o,b // Z by A3, AFF_1:66;
then Y // Z by A3, A320, AFF_1:67;
hence contradiction by A3, AFF_1:59; :: thesis: verum

end;

b,d // b,d5

proof

A321: b <> c by A4, AFF_1:12;
A322: b,c // b,d by A286, AFF_1:def 1;
b,c // b,d5 by A310, AFF_1:def 1;
hence b,d // b,d5 by A321, A322, AFF_1:14; :: thesis: verum

end;

then LIN d1,d2,d by A310, A313, A314, AFF_1:23;
then LIN d,d1,d2 by AFF_1:15;
then A323: d,d1 // d,d2 by AFF_1:def 1;
A324: o <> d

proof

assume A325: o = d ; :: thesis: contradiction
then LIN o,b,c by A286, AFF_1:15;
then A326: o,b // o,c by AFF_1:def 1;
A327: ( o,b // o,b1 & o,c // o,c1 ) by A3, A242, AFF_1:53;
then o,b1 // o,c by A3, A326, AFF_1:14;
then o,b1 // o,c1 by A3, A327, AFF_1:14;
then LIN o,b1,c1 by AFF_1:def 1;
then LIN b1,c1,o by AFF_1:15;
then b1,c1 // b1,o by AFF_1:def 1;
then A328: b1,c1 // o,b1 by AFF_1:13;
b,c // b,o by A286, A325, AFF_1:def 1;
then b,c // o,b by AFF_1:13;
then b,c // o,b1 by A3, A327, AFF_1:14;
hence contradiction by A4, A264, A328, AFF_1:14; :: thesis: verum

end;

A329: d <> d1

proof

assume d = d1 ; :: thesis: contradiction
then A330: o,d // Z by A3, A292, AFF_1:66;
o,d // Y by A3, A311, AFF_1:66;
then Y // Z by A324, A330, AFF_1:67;
hence contradiction by A3, AFF_1:59; :: thesis: verum

end;

A331: d <> d2

proof

assume d = d2 ; :: thesis: contradiction
then A332: o,d // M by A3, A297, AFF_1:66;
o,d // Y by A3, A311, AFF_1:66;
then Y // M by A324, A332, AFF_1:67;
hence contradiction by A3, AFF_1:59; :: thesis: verum

end;

a,b // d,d2 by A292, A323, A329, AFF_1:14;
then A333: a,b // a,c by A297, A331, AFF_1:14;
then a1,b1 // a,c by A3, A243, AFF_1:14;
then a1,b1 // a1,c1 by A3, A243, AFF_1:14;
then LIN a1,b1,c1 by AFF_1:def 1;
then LIN b1,c1,a1 by AFF_1:15;
then b1,c1 // b1,a1 by AFF_1:def 1;
then A334: b1,c1 // a1,b1 by AFF_1:13;
A335: a1 <> b1

proof

assume A336: a1 = b1 ; :: thesis: contradiction
o,a1 // o,a by A3, A242, AFF_1:53;
then LIN o,a1,a by AFF_1:def 1;
hence contradiction by A3, A243, A264, A336, AFF_1:39; :: thesis: verum

end;

LIN a,b,c by A333, 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 b,c // a1,b1 by A3, A243, AFF_1:14;
hence contradiction by A4, A334, A335, AFF_1:14; :: thesis: verum

end;

not b,c // d1,d2 by A4, A298, A306, AFF_1:14;
hence contradiction by A2, A3, A5, A292, A297, A310, A311, A312; :: thesis: verum

end;

now

assume A337: not b1,c1 // d1,d2 ; :: thesis: contradiction
then consider d5 being Element of X such that
A338: ( LIN b1,c1,d5 & LIN d1,d2,d5 ) by AFF_1:74;
A339: d in Y by A3, A248, A287, AFF_1:39;
A340: a1,b1 // d,d1 by A3, A243, A292, AFF_1:14;
a1,c1 // d,d2 by A3, A243, A297, AFF_1:14;
then A341: LIN a1,d,d5 by A2, A3, A5, A264, A292, A297, A337, A338, A339, A340;
A342: not LIN a1,b1,d

proof

assume LIN a1,b1,d ; :: thesis: contradiction
then A343: LIN a1,d,b1 by AFF_1:15;
a1 <> d

proof

assume A344: a1 = d ; :: thesis: contradiction
then LIN a1,b1,c1 by A286, AFF_1:15;
then A345: a1,b1 // a1,c1 by AFF_1:def 1;
A346: ( a1 <> b1 & a1 <> c1 )

proof

assume A347: ( not a1 <> b1 or not a1 <> c1 ) ; :: thesis: contradiction
o,a1 // o,a by A3, A242, AFF_1:53;
then LIN o,a1,a by AFF_1:def 1;
hence contradiction by A3, A243, A264, A347, AFF_1:39; :: thesis: verum

end;

then a,b // a1,c1 by A3, A345, AFF_1:14;
then a,b // a,c by A3, A346, 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 A348: b,c // a,b by AFF_1:13;
b1,c1 // b1,a1 by A286, A344, AFF_1:def 1;
then b1,c1 // a1,b1 by AFF_1:13;
then b1,c1 // a,b by A3, A346, AFF_1:14;
hence contradiction by A3, A4, A243, A348, AFF_1:14; :: thesis: verum

end;

then b1 in Y by A3, A339, A343, AFF_1:39;
then o,b1 // o,a by A3, A242, AFF_1:53;
then LIN o,b1,a by AFF_1:def 1;
hence contradiction by A3, A243, A264, AFF_1:39; :: thesis: verum

end;

b1,d // b1,d5

proof

A349: b1 <> c1 by A4, AFF_1:12;
A350: b1,c1 // b1,d5 by A338, AFF_1:def 1;
b1,c1 // b1,d by A286, AFF_1:def 1;
hence b1,d // b1,d5 by A349, A350, AFF_1:14; :: thesis: verum

end;

then d = d5 by A341, A342, AFF_1:23;
then LIN d,d1,d2 by A338, AFF_1:15;
then A351: d,d1 // d,d2 by AFF_1:def 1;
A352: d <> o

proof

assume A353: d = o ; :: thesis: contradiction
then LIN o,b,c by A286, AFF_1:15;
then A354: o,b // o,c by AFF_1:def 1;
A355: ( o,b // o,b1 & o,c // o,c1 ) by A3, A242, AFF_1:53;
then o,b1 // o,c by A3, A354, AFF_1:14;
then o,b1 // o,c1 by A3, A355, AFF_1:14;
then LIN o,b1,c1 by AFF_1:def 1;
then LIN b1,c1,o by AFF_1:15;
then b1,c1 // b1,o by AFF_1:def 1;
then A356: b1,c1 // o,b1 by AFF_1:13;
b,c // b,o by A286, A353, AFF_1:def 1;
then b,c // o,b by AFF_1:13;
then b,c // o,b1 by A3, A355, AFF_1:14;
hence contradiction by A4, A264, A356, AFF_1:14; :: thesis: verum

end;

A357: d <> d1

proof

assume A358: d = d1 ; :: thesis: contradiction
o,d // o,a by A3, A242, A339, AFF_1:53;
then LIN o,d,a by AFF_1:def 1;
hence contradiction by A3, A243, A292, A352, A358, AFF_1:39; :: thesis: verum

end;

A359: d <> d2

proof

assume A360: d = d2 ; :: thesis: contradiction
o,d // o,a by A3, A242, A339, AFF_1:53;
then LIN o,d,a by AFF_1:def 1;
hence contradiction by A3, A243, A297, A352, A360, AFF_1:39; :: thesis: verum

end;

a,b // d,d2 by A292, A351, A357, AFF_1:14;
then A361: a,b // a,c by A297, A359, AFF_1:14;
A362: a1 <> b1

proof

assume A363: a1 = b1 ; :: thesis: contradiction
o,a1 // o,a by A3, A242, AFF_1:53;
then LIN o,a1,a by AFF_1:def 1;
hence contradiction by A3, A243, A264, A363, AFF_1:39; :: thesis: verum

end;

a1,b1 // a,c by A3, A243, A361, AFF_1:14;
then a1,b1 // a1,c1 by A3, A243, AFF_1:14;
then LIN a1,b1,c1 by AFF_1:def 1;
then LIN b1,c1,a1 by AFF_1:15;
then b1,c1 // b1,a1 by AFF_1:def 1;
then A364: b1,c1 // a1,b1 by AFF_1:13;
LIN a,b,c by A361, 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 b,c // a1,b1 by A3, A243, AFF_1:14;
hence contradiction by A4, A362, A364, AFF_1:14; :: thesis: verum

end;

hence contradiction by A305; :: thesis: verum

end;

hence contradiction by A239; :: thesis: verum

end;

hence X is Desarguesian by AFF_2:def 4; :: thesis: verum

end;

( X is Desarguesian implies X is satisfying_Scherungssatz )

proof

assume A365: X is Desarguesian ; :: thesis: X is satisfying_Scherungssatz
then X is Moufangian by AFF_2:26;
then X is satisfying_TDES_1 by AFF_2:17;
then X is satisfying_des_1 by AFF_2:27;
then X is translational by AFF_2:21;
then A366: X is satisfying_minor_Scherungssatz by Th6;
X is satisfying_major_Scherungssatz by A365, Th7;
hence X is satisfying_Scherungssatz by A366, Th2; :: thesis: verum

end;

hence ( X is Desarguesian iff X is satisfying_Scherungssatz ) by A1; :: thesis: verum