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 :: thesis: for Y, Z, M being Subset of X
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 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 that
A3: o in Y and
A4: o in Z and
A5: o in M and
A6: o <> a and
A7: o <> b and
A8: o <> c and
A9: a in Y and
A10: a1 in Y and
A11: b in Z and
A12: b1 in Z and
A13: c in M and
A14: c1 in M and
A15: Y is being_line and
A16: Z is being_line and
A17: M is being_line and
A18: Y <> Z and
A19: Y <> M and
A20: a,b // a1,b1 and
A21: a,c // a1,c1 ; :: thesis: b,c // b1,c1
assume A22: not b,c // b1,c1 ; :: thesis: contradiction

A23: now :: thesis: for Y, Z, M being Subset of X
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 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 A24: 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 that
A25: o in Y and
A26: o in Z and
A27: o in M and
A28: o <> a and
A29: o <> b and
A30: o <> c and
A31: a in Y and
A32: a1 in Y and
A33: b in Z and
A34: b1 in Z and
A35: c in M and
A36: c1 in M and
A37: Y is being_line and
A38: Z is being_line and
A39: M is being_line and
A40: Y <> Z and
A41: Y <> M and
A42: a,b // a1,b1 and
A43: a,c // a1,c1 and
A44: LIN b,c,d and
A45: 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 that
A46: not LIN a,a1,d and
A47: not b,c // b1,c1 ; :: thesis: contradiction
A48: ( c <> c1 & a <> a1 & b <> b1 )

proof

A49: now :: thesis: not b = b1

A50: not LIN o,a,c

proof

assume LIN o,a,c ; :: thesis: contradiction
then c in Y by A25, A28, A31, A37, AFF_1:25;
then A51: o,c // Y by A25, A37, AFF_1:52;
o,c // M by A27, A35, A39, AFF_1:52;
hence contradiction by A25, A27, A30, A41, A51, AFF_1:45, AFF_1:53; :: thesis: verum

end;

o,c // o,c1 by A27, A35, A36, A39, AFF_1:39, AFF_1:41;
then A52: LIN o,c,c1 by AFF_1:def 1;
A53: not LIN o,b,a

proof

assume LIN o,b,a ; :: thesis: contradiction
then a in Z by A26, A29, A33, A38, AFF_1:25;
then A54: o,a // Z by A26, A38, AFF_1:52;
o,a // Y by A25, A31, A37, AFF_1:52;
hence contradiction by A25, A26, A28, A40, A54, AFF_1:45, AFF_1:53; :: thesis: verum

end;

o,a // o,a1 by A25, A31, A32, A37, AFF_1:39, AFF_1:41;
then A55: LIN o,a,a1 by AFF_1:def 1;
assume A56: b = b1 ; :: thesis: contradiction
then b,a // b,a1 by A42, AFF_1:4;
then a = a1 by A53, A55, AFF_1:14;
then c = c1 by A43, A50, A52, AFF_1:14;
hence contradiction by A47, A56, AFF_1:2; :: thesis: verum

end;

A57: now :: thesis: not c = c1

A58: not LIN o,a,b

proof

assume LIN o,a,b ; :: thesis: contradiction
then b in Y by A25, A28, A31, A37, AFF_1:25;
then A59: o,b // Y by A25, A37, AFF_1:52;
o,b // Z by A26, A33, A38, AFF_1:52;
hence contradiction by A25, A26, A29, A40, A59, AFF_1:45, AFF_1:53; :: thesis: verum

end;

o,b // o,b1 by A26, A33, A34, A38, AFF_1:39, AFF_1:41;
then A60: LIN o,b,b1 by AFF_1:def 1;
A61: not LIN o,c,a

proof

assume LIN o,c,a ; :: thesis: contradiction
then a in M by A27, A30, A35, A39, AFF_1:25;
then A62: o,a // M by A27, A39, AFF_1:52;
o,a // Y by A25, A31, A37, AFF_1:52;
hence contradiction by A25, A27, A28, A41, A62, AFF_1:45, AFF_1:53; :: thesis: verum

end;

o,a // o,a1 by A25, A31, A32, A37, AFF_1:39, AFF_1:41;
then A63: LIN o,a,a1 by AFF_1:def 1;
assume A64: c = c1 ; :: thesis: contradiction
then c,a // c,a1 by A43, AFF_1:4;
then a = a1 by A61, A63, AFF_1:14;
then b = b1 by A42, A58, A60, AFF_1:14;
hence contradiction by A47, A64, AFF_1:2; :: thesis: verum

end;

A65: now :: thesis: not a = a1

A66: not LIN o,a,c

proof

assume LIN o,a,c ; :: thesis: contradiction
then c in Y by A25, A28, A31, A37, AFF_1:25;
then A67: o,c // Y by A25, A37, AFF_1:52;
o,c // M by A27, A35, A39, AFF_1:52;
hence contradiction by A25, A27, A30, A41, A67, AFF_1:45, AFF_1:53; :: thesis: verum

end;

A68: not LIN o,a,b

proof

assume LIN o,a,b ; :: thesis: contradiction
then b in Y by A25, A28, A31, A37, AFF_1:25;
then A69: o,b // Y by A25, A37, AFF_1:52;
o,b // Z by A26, A33, A38, AFF_1:52;
hence contradiction by A25, A26, A29, A40, A69, AFF_1:45, AFF_1:53; :: thesis: verum

end;

assume A70: a = a1 ; :: thesis: contradiction
o,c // o,c1 by A27, A35, A36, A39, AFF_1:39, AFF_1:41;
then LIN o,c,c1 by AFF_1:def 1;
then A71: c = c1 by A43, A70, A66, AFF_1:14;
o,b // o,b1 by A26, A33, A34, A38, AFF_1:39, AFF_1:41;
then LIN o,b,b1 by AFF_1:def 1;
then b = b1 by A42, A70, A68, AFF_1:14;
hence contradiction by A47, A71, AFF_1:2; :: thesis: verum

end;

assume ( not c <> c1 or not a <> a1 or not b <> b1 ) ; :: thesis: contradiction
hence contradiction by A57, A65, A49; :: thesis: verum

end;

now :: thesis: not b <> c

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

A73: now :: thesis: not b1 <> o

assume A74: b1 <> o ; :: thesis: contradiction
A75: ( a1 <> b1 & a1 <> c1 )

proof

A76: now :: thesis: not a1 = c1

A77: o <> a1

proof

A78: not LIN a,b,o

proof

assume LIN a,b,o ; :: thesis: contradiction
then LIN o,a,b by AFF_1:6;
then b in Y by A25, A28, A31, A37, AFF_1:25;
then A79: o,b // Y by A25, A37, AFF_1:52;
o,b // Z by A26, A33, A38, AFF_1:52;
hence contradiction by A25, A26, A29, A40, A79, AFF_1:45, AFF_1:53; :: thesis: verum

end;

A80: o,b // o,b1 by A26, A33, A34, A38, AFF_1:39, AFF_1:41;
assume o = a1 ; :: thesis: contradiction
then a,b // o,b by A42, A74, A80, AFF_1:5;
then b,a // b,o by AFF_1:4;
then LIN b,a,o by AFF_1:def 1;
then LIN o,a,b by AFF_1:6;
then o,a // o,b by AFF_1:def 1;
then o,a // o,b1 by A29, A80, AFF_1:5;
then LIN o,a,b1 by AFF_1:def 1;
then A81: LIN a,o,b1 by AFF_1:6;
b,o // b,b1 by A26, A33, A34, A38, AFF_1:39, AFF_1:41;
hence contradiction by A74, A78, A81, AFF_1:14; :: thesis: verum

end;

assume a1 = c1 ; :: thesis: contradiction
then A82: o,a1 // M by A27, A36, A39, AFF_1:52;
o,a1 // Y by A25, A32, A37, AFF_1:52;
hence contradiction by A25, A27, A41, A82, A77, AFF_1:45, AFF_1:53; :: thesis: verum

end;

A83: now :: thesis: not a1 = b1

assume a1 = b1 ; :: thesis: contradiction
then A84: o,b1 // Y by A25, A32, A37, AFF_1:52;
o,b1 // Z by A26, A34, A38, AFF_1:52;
hence contradiction by A25, A26, A40, A74, A84, AFF_1:45, AFF_1:53; :: thesis: verum

end;

assume ( not a1 <> b1 or not a1 <> c1 ) ; :: thesis: contradiction
hence contradiction by A83, A76; :: thesis: verum

end;

LIN o,o,a by AFF_1:7;
then consider C being Subset of X such that
A85: C is being_line and
A86: o in C and
o in C and
A87: a in C by AFF_1:21;
A88: ex d2 being Element of X st
( d2 in C & a,c // d,d2 )

proof

consider e2 being Element of X such that
A89: a,c // d,e2 and
A90: d <> e2 by DIRAF:40;
consider e1 being Element of X such that
A91: o,a // o,e1 and
A92: o <> e1 by DIRAF:40;
LIN o,a,e1 by A91, AFF_1:def 1;
then A93: e1 in C by A28, A85, A86, A87, AFF_1:25;
not o,e1 // d,e2

proof

assume o,e1 // d,e2 ; :: thesis: contradiction
then o,a // d,e2 by A91, A92, AFF_1:5;
then o,a // a,c by A89, A90, AFF_1:5;
then a,o // a,c by AFF_1:4;
then LIN a,o,c by AFF_1:def 1;
then c in Y by A25, A28, A31, A37, AFF_1:25;
then A94: o,c // Y by A25, A37, AFF_1:52;
o,c // M by A27, A35, A39, AFF_1:52;
hence contradiction by A25, A27, A30, A41, A94, AFF_1:45, AFF_1:53; :: thesis: verum

end;

then consider d2 being Element of X such that
A95: LIN o,e1,d2 and
A96: LIN d,e2,d2 by AFF_1:60;
take d2 ; :: thesis: ( d2 in C & a,c // d,d2 )
d,e2 // d,d2 by A96, AFF_1:def 1;
hence ( d2 in C & a,c // d,d2 ) by A85, A86, A92, A89, A90, A95, A93, AFF_1:5, AFF_1:25; :: thesis: verum

end;

A97: ex d1 being Element of X st
( d1 in C & c,c1 // d,d1 )

proof

consider e2 being Element of X such that
A98: c,c1 // d,e2 and
A99: d <> e2 by DIRAF:40;
consider e1 being Element of X such that
A100: o,a // o,e1 and
A101: o <> e1 by DIRAF:40;
LIN o,a,e1 by A100, AFF_1:def 1;
then A102: e1 in C by A28, A85, A86, A87, AFF_1:25;
not o,e1 // d,e2

proof

assume o,e1 // d,e2 ; :: thesis: contradiction
then o,a // d,e2 by A100, A101, AFF_1:5;
then A103: o,a // c,c1 by A98, A99, AFF_1:5;
c,c1 // o,c by A27, A35, A36, A39, AFF_1:39, AFF_1:41;
then o,a // o,c by A48, A103, AFF_1:5;
then LIN o,a,c by AFF_1:def 1;
then c in Y by A25, A28, A31, A37, AFF_1:25;
then A104: o,c // Y by A25, A37, AFF_1:52;
o,c // M by A27, A35, A39, AFF_1:52;
hence contradiction by A25, A27, A30, A41, A104, AFF_1:45, AFF_1:53; :: thesis: verum

end;

then consider d1 being Element of X such that
A105: LIN o,e1,d1 and
A106: LIN d,e2,d1 by AFF_1:60;
take d1 ; :: thesis: ( d1 in C & c,c1 // d,d1 )
d,e2 // d,d1 by A106, AFF_1:def 1;
hence ( d1 in C & c,c1 // d,d1 ) by A85, A86, A101, A98, A99, A105, A102, AFF_1:5, AFF_1:25; :: thesis: verum

end;

consider d2 being Element of X such that
A107: d2 in C and
A108: a,c // d,d2 by A88;
consider d1 being Element of X such that
A109: d1 in C and
A110: c,c1 // d,d1 by A97;
c,c1 // c,o by A27, A35, A36, A39, AFF_1:39, AFF_1:41;
then A111: c,o // d,d1 by A48, A110, AFF_1:5;
o,a // o,a1 by A25, A31, A32, A37, AFF_1:39, AFF_1:41;
then LIN o,a,a1 by AFF_1:def 1;
then A112: a1 in C by A28, A85, A86, A87, AFF_1:25;
LIN b,b,c by AFF_1:7;
then consider A being Subset of X such that
A113: A is being_line and
A114: b in A and
b in A and
A115: c in A by AFF_1:21;
A116: d in A by A44, A72, A113, A114, A115, AFF_1:25;
A117: b <> c by A47, AFF_1:3;
A118: ex d3 being Element of X st
( d3 in A & o,b // d1,d3 )

proof

consider e2 being Element of X such that
A119: o,b // d1,e2 and
A120: d1 <> e2 by DIRAF:40;
consider e1 being Element of X such that
A121: b,c // b,e1 and
A122: b <> e1 by DIRAF:40;
LIN b,c,e1 by A121, AFF_1:def 1;
then A123: e1 in A by A117, A113, A114, A115, AFF_1:25;
not b,e1 // d1,e2

proof

assume b,e1 // d1,e2 ; :: thesis: contradiction
then b,c // d1,e2 by A121, A122, AFF_1:5;
then A124: b,c // o,b by A119, A120, AFF_1:5;
then b,c // b,o by AFF_1:4;
then LIN b,c,o by AFF_1:def 1;
then LIN o,b,c by AFF_1:6;
then A125: o,b // o,c by AFF_1:def 1;
A126: o,b // o,b1 by A26, A33, A34, A38, AFF_1:39, AFF_1:41;
o,c // o,c1 by A27, A35, A36, A39, AFF_1:39, AFF_1:41;
then o,b // o,c1 by A30, A125, AFF_1:5;
then o,b1 // o,c1 by A29, A126, AFF_1:5;
then LIN o,b1,c1 by AFF_1:def 1;
then LIN b1,c1,o by AFF_1:6;
then b1,c1 // b1,o by AFF_1:def 1;
then b1,c1 // o,b1 by AFF_1:4;
then b1,c1 // o,b by A74, A126, AFF_1:5;
hence contradiction by A29, A47, A124, AFF_1:5; :: thesis: verum

end;

then consider d3 being Element of X such that
A127: LIN b,e1,d3 and
A128: LIN d1,e2,d3 by AFF_1:60;
take d3 ; :: thesis: ( d3 in A & o,b // d1,d3 )
d1,e2 // d1,d3 by A128, AFF_1:def 1;
hence ( d3 in A & o,b // d1,d3 ) by A113, A114, A122, A119, A120, A127, A123, AFF_1:5, AFF_1:25; :: thesis: verum

end;

A129: ( not o in A & not a in A & not d1 in A & not d2 in A )

proof

A130: now :: thesis: not a in A

A131: a <> b

proof

assume a = b ; :: thesis: contradiction
then A132: o,b // Y by A25, A31, A37, AFF_1:52;
o,b // Z by A26, A33, A38, AFF_1:52;
hence contradiction by A25, A26, A29, A40, A132, AFF_1:45, AFF_1:53; :: thesis: verum

end;

A133: a1 <> b1

proof

assume a1 = b1 ; :: thesis: contradiction
then A134: o,b1 // Y by A25, A32, A37, AFF_1:52;
o,b1 // Z by A26, A34, A38, AFF_1:52;
hence contradiction by A25, A26, A40, A74, A134, AFF_1:45, AFF_1:53; :: thesis: verum

end;

assume a in A ; :: thesis: contradiction
then A135: a,b // a,c by A113, A114, A115, AFF_1:39, AFF_1:41;
a <> c

proof

assume a = c ; :: thesis: contradiction
then A136: o,c // Y by A25, A31, A37, AFF_1:52;
o,c // M by A27, A35, A39, AFF_1:52;
hence contradiction by A25, A27, A30, A41, A136, AFF_1:45, AFF_1:53; :: thesis: verum

end;

then a,b // a1,c1 by A43, A135, AFF_1:5;
then a1,b1 // a1,c1 by A42, A131, AFF_1:5;
then LIN a1,b1,c1 by AFF_1:def 1;
then LIN b1,c1,a1 by AFF_1:6;
then b1,c1 // b1,a1 by AFF_1:def 1;
then A137: a1,b1 // b1,c1 by AFF_1:4;
LIN a,b,c by A135, 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 b,c // a1,b1 by A42, A131, AFF_1:5;
hence contradiction by A47, A137, A133, AFF_1:5; :: thesis: verum

end;

A138: now :: thesis: not d2 in A

A139: d <> d2

proof

o,a // o,a1 by A25, A31, A32, A37, AFF_1:39, AFF_1:41;
then LIN o,a,a1 by AFF_1:def 1;
then A140: a1 in C by A28, A85, A86, A87, AFF_1:25;
assume d = d2 ; :: thesis: contradiction
then a,a1 // a,d by A85, A87, A107, A140, AFF_1:39, AFF_1:41;
hence contradiction by A46, AFF_1:def 1; :: thesis: verum

end;

assume A141: d2 in A ; :: thesis: contradiction
A142: d,d2 // c,a by A108, AFF_1:4;
d in A by A44, A117, A113, A114, A115, AFF_1:25;
hence contradiction by A113, A115, A130, A141, A139, A142, AFF_1:48; :: thesis: verum

end;

A143: now :: thesis: not o in A

assume o in A ; :: thesis: contradiction
then A144: o,b // o,c by A113, A114, A115, AFF_1:39, AFF_1:41;
A145: o,b // o,b1 by A26, A33, A34, A38, AFF_1:39, AFF_1:41;
o,c // o,c1 by A27, A35, A36, A39, AFF_1:39, AFF_1:41;
then o,b // o,c1 by A30, A144, AFF_1:5;
then o,b1 // o,c1 by A29, A145, AFF_1:5;
then LIN o,b1,c1 by AFF_1:def 1;
then LIN b1,c1,o by AFF_1:6;
then b1,c1 // b1,o by AFF_1:def 1;
then b1,c1 // o,b1 by AFF_1:4;
then o,b // b1,c1 by A74, A145, AFF_1:5;
then A146: b,o // b1,c1 by AFF_1:4;
LIN o,b,c by A144, AFF_1:def 1;
then LIN b,c,o by AFF_1:6;
then b,c // b,o by AFF_1:def 1;
hence contradiction by A29, A47, A146, AFF_1:5; :: thesis: verum

end;

A147: now :: thesis: not d1 in A

A148: d <> d1

proof

o,a // o,a1 by A25, A31, A32, A37, AFF_1:39, AFF_1:41;
then LIN o,a,a1 by AFF_1:def 1;
then A149: a1 in C by A28, A85, A86, A87, AFF_1:25;
assume d = d1 ; :: thesis: contradiction
then a,a1 // a,d by A85, A87, A109, A149, AFF_1:39, AFF_1:41;
hence contradiction by A46, AFF_1:def 1; :: thesis: verum

end;

assume A150: d1 in A ; :: thesis: contradiction
c,c1 // c,o by A27, A35, A36, A39, AFF_1:39, AFF_1:41;
then A151: LIN c,c1,o by AFF_1:def 1;
A152: d,d1 // c,c1 by A110, AFF_1:4;
d in A by A44, A117, A113, A114, A115, AFF_1:25;
then c1 in A by A113, A115, A150, A148, A152, AFF_1:48;
hence contradiction by A48, A113, A115, A143, A151, AFF_1:25; :: thesis: verum

end;

assume ( o in A or a in A or d1 in A or d2 in A ) ; :: thesis: contradiction
hence contradiction by A143, A130, A147, A138; :: thesis: verum

end;

LIN b1,b1,c1 by AFF_1:7;
then consider K being Subset of X such that
A153: K is being_line and
A154: b1 in K and
b1 in K and
A155: c1 in K by AFF_1:21;
b1 <> c1 by A47, AFF_1:3;
then A156: d in K by A45, A153, A154, A155, AFF_1:25;
consider d3 being Element of X such that
A157: d3 in A and
A158: o,b // d1,d3 by A118;
A159: b1 <> c1 by A47, AFF_1:3;
ex d4 being Element of X st
( d4 in K & d1,d3 // d1,d4 )

proof

consider e2 being Element of X such that
A160: d1,d3 // d1,e2 and
A161: d1 <> e2 by DIRAF:40;
consider e1 being Element of X such that
A162: b1,c1 // b1,e1 and
A163: b1 <> e1 by DIRAF:40;
LIN b1,c1,e1 by A162, AFF_1:def 1;
then A164: e1 in K by A159, A153, A154, A155, AFF_1:25;
not b1,e1 // d1,e2

proof

A165: o <> c1

proof

A166: not LIN a,c,o

proof

assume LIN a,c,o ; :: thesis: contradiction
then LIN o,a,c by AFF_1:6;
then c in Y by A25, A28, A31, A37, AFF_1:25;
then A167: o,c // Y by A25, A37, AFF_1:52;
o,c // M by A27, A35, A39, AFF_1:52;
hence contradiction by A25, A27, A30, A41, A167, AFF_1:45, AFF_1:53; :: thesis: verum

end;

assume A168: o = c1 ; :: thesis: contradiction
a1,o // a,a1 by A25, A31, A32, A37, AFF_1:39, AFF_1:41;
then a,c // a,a1 by A43, A75, A168, AFF_1:5;
then LIN a,c,a1 by AFF_1:def 1;
then LIN a1,c,a by AFF_1:6;
then A169: a1,c // a1,a by AFF_1:def 1;
a1,a // a1,o by A25, A31, A32, A37, AFF_1:39, AFF_1:41;
then a1,c // a1,o by A48, A169, AFF_1:5;
then LIN a1,c,o by AFF_1:def 1;
then LIN c,o,a1 by AFF_1:6;
then A170: c,o // c,a1 by AFF_1:def 1;
a,o // a,a1 by A25, A31, A32, A37, AFF_1:39, AFF_1:41;
then LIN a,o,a1 by AFF_1:def 1;
hence contradiction by A75, A168, A166, A170, AFF_1:14; :: thesis: verum

end;

A171: d1 <> d3

proof

A172: d <> d1

proof

o,a // o,a1 by A25, A31, A32, A37, AFF_1:39, AFF_1:41;
then LIN o,a,a1 by AFF_1:def 1;
then A173: a1 in C by A28, A85, A86, A87, AFF_1:25;
assume d = d1 ; :: thesis: contradiction
then a,a1 // a,d by A85, A87, A109, A173, AFF_1:39, AFF_1:41;
hence contradiction by A46, AFF_1:def 1; :: thesis: verum

end;

assume A174: d1 = d3 ; :: thesis: contradiction
c,c1 // o,c by A27, A35, A36, A39, AFF_1:39, AFF_1:41;
then o,c // d,d1 by A48, A110, AFF_1:5;
then A175: d,d1 // c,o by AFF_1:4;
A176: o,b // o,b1 by A26, A33, A34, A38, AFF_1:39, AFF_1:41;
d in A by A44, A117, A113, A114, A115, AFF_1:25;
then o in A by A113, A115, A157, A174, A172, A175, AFF_1:48;
then A177: o,b // o,c by A113, A114, A115, AFF_1:39, AFF_1:41;
o,c // o,c1 by A27, A35, A36, A39, AFF_1:39, AFF_1:41;
then o,b // o,c1 by A30, A177, AFF_1:5;
then o,b1 // o,c1 by A29, A176, AFF_1:5;
then LIN o,b1,c1 by AFF_1:def 1;
then LIN b1,c1,o by AFF_1:6;
then b1,c1 // b1,o by AFF_1:def 1;
then b1,c1 // o,b1 by AFF_1:4;
then A178: o,b // b1,c1 by A74, A176, AFF_1:5;
LIN o,b,c by A177, AFF_1:def 1;
then LIN b,c,o by AFF_1:6;
then b,c // b,o by AFF_1:def 1;
then b,c // o,b by AFF_1:4;
hence contradiction by A29, A47, A178, AFF_1:5; :: thesis: verum

end;

assume b1,e1 // d1,e2 ; :: thesis: contradiction
then b1,c1 // d1,e2 by A162, A163, AFF_1:5;
then A179: b1,c1 // d1,d3 by A160, A161, AFF_1:5;
A180: o,b // o,b1 by A26, A33, A34, A38, AFF_1:39, AFF_1:41;
then o,b1 // d1,d3 by A29, A158, AFF_1:5;
then A181: o,b1 // b1,c1 by A179, A171, AFF_1:5;
then b1,o // b1,c1 by AFF_1:4;
then LIN b1,o,c1 by AFF_1:def 1;
then LIN o,b1,c1 by AFF_1:6;
then o,b1 // o,c1 by AFF_1:def 1;
then A182: o,b // o,c1 by A74, A180, AFF_1:5;
o,c // o,c1 by A27, A35, A36, A39, AFF_1:39, AFF_1:41;
then o,b // o,c by A182, A165, AFF_1:5;
then LIN o,b,c by AFF_1:def 1;
then LIN b,o,c by AFF_1:6;
then b,o // b,c by AFF_1:def 1;
then o,b // b,c by AFF_1:4;
then o,b1 // b,c by A29, A180, AFF_1:5;
hence contradiction by A47, A74, A181, AFF_1:5; :: thesis: verum

end;

then consider d4 being Element of X such that
A183: LIN b1,e1,d4 and
A184: LIN d1,e2,d4 by AFF_1:60;
take d4 ; :: thesis: ( d4 in K & d1,d3 // d1,d4 )
d1,e2 // d1,d4 by A184, AFF_1:def 1;
hence ( d4 in K & d1,d3 // d1,d4 ) by A153, A154, A163, A160, A161, A183, A164, AFF_1:5, AFF_1:25; :: thesis: verum

end;

then consider d4 being Element of X such that
A185: d4 in K and
A186: d1,d3 // d1,d4 ;
A187: ( not c in C & not b in C & not d in C & not d3 in C )

proof

A188: now :: thesis: not b in C

assume b in C ; :: thesis: contradiction
then o,a // o,b by A85, A86, A87, AFF_1:39, AFF_1:41;
then LIN o,a,b by AFF_1:def 1;
then b in Y by A25, A28, A31, A37, AFF_1:25;
then A189: o,b // Y by A25, A37, AFF_1:52;
o,b // Z by A26, A33, A38, AFF_1:52;
hence contradiction by A25, A26, A29, A40, A189, AFF_1:45, AFF_1:53; :: thesis: verum

end;

A190: now :: thesis: not d3 in C

A191: d1 <> d3

proof

A192: d <> d1

proof

o,a // o,a1 by A25, A31, A32, A37, AFF_1:39, AFF_1:41;
then LIN o,a,a1 by AFF_1:def 1;
then A193: a1 in C by A28, A85, A86, A87, AFF_1:25;
assume d = d1 ; :: thesis: contradiction
then a,a1 // a,d by A85, A87, A109, A193, AFF_1:39, AFF_1:41;
hence contradiction by A46, AFF_1:def 1; :: thesis: verum

end;

assume A194: d1 = d3 ; :: thesis: contradiction
A195: o,c // o,c1 by A27, A35, A36, A39, AFF_1:39, AFF_1:41;
A196: d,d1 // c,c1 by A110, AFF_1:4;
d in A by A44, A117, A113, A114, A115, AFF_1:25;
then c1 in A by A113, A115, A157, A194, A192, A196, AFF_1:48;
then A197: c,c1 // c,b by A113, A114, A115, AFF_1:39, AFF_1:41;
A198: o,b // o,b1 by A26, A33, A34, A38, AFF_1:39, AFF_1:41;
c,o // c,c1 by A27, A35, A36, A39, AFF_1:39, AFF_1:41;
then c,o // c,b by A48, A197, AFF_1:5;
then A199: LIN c,o,b by AFF_1:def 1;
then LIN o,b,c by AFF_1:6;
then o,b // o,c by AFF_1:def 1;
then o,b1 // o,c by A29, A198, AFF_1:5;
then o,b1 // o,c1 by A30, A195, AFF_1:5;
then LIN o,b1,c1 by AFF_1:def 1;
then LIN b1,c1,o by AFF_1:6;
then b1,c1 // b1,o by AFF_1:def 1;
then b1,c1 // o,b1 by AFF_1:4;
then A200: o,b // b1,c1 by A74, A198, AFF_1:5;
LIN b,c,o by A199, AFF_1:6;
then b,c // b,o by AFF_1:def 1;
then b,c // o,b by AFF_1:4;
hence contradiction by A29, A47, A200, AFF_1:5; :: thesis: verum

end;

assume A201: d3 in C ; :: thesis: contradiction
d1,d3 // o,b by A158, AFF_1:4;
hence contradiction by A85, A86, A109, A188, A201, A191, AFF_1:48; :: thesis: verum

end;

A202: now :: thesis: not c in C

assume c in C ; :: thesis: contradiction
then o,a // o,c by A85, A86, A87, AFF_1:39, AFF_1:41;
then LIN o,a,c by AFF_1:def 1;
then c in Y by A25, A28, A31, A37, AFF_1:25;
then A203: o,c // Y by A25, A37, AFF_1:52;
o,c // M by A27, A35, A39, AFF_1:52;
hence contradiction by A25, A27, A30, A41, A203, AFF_1:45, AFF_1:53; :: thesis: verum

end;

A204: now :: thesis: not d in C

assume d in C ; :: thesis: contradiction
then A205: o,a // a,d by A85, A86, A87, AFF_1:39, AFF_1:41;
o,a // a,a1 by A25, A31, A32, A37, AFF_1:39, AFF_1:41;
then a,a1 // a,d by A28, A205, AFF_1:5;
hence contradiction by A46, AFF_1:def 1; :: thesis: verum

end;

assume ( c in C or b in C or d in C or d3 in C ) ; :: thesis: contradiction
hence contradiction by A202, A188, A204, A190; :: thesis: verum

end;

A206: d4 <> d3

proof

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

proof

d in A by A44, A117, A113, A114, A115, AFF_1:25;
then A208: b,c // d,d3 by A113, A114, A115, A157, AFF_1:39, AFF_1:41;
d in K by A45, A159, A153, A154, A155, AFF_1:25;
then A209: b1,c1 // d,d3 by A153, A154, A155, A185, A207, AFF_1:39, AFF_1:41;
assume d <> d3 ; :: thesis: contradiction
hence contradiction by A47, A209, A208, AFF_1:5; :: thesis: verum

end;

then A210: o,b // d,d1 by A158, AFF_1:4;
o,c // c,c1 by A27, A35, A36, A39, AFF_1:39, AFF_1:41;
then o,c // d,d1 by A48, A110, AFF_1:5;
then A211: o,b // o,c by A109, A187, A210, AFF_1:5;
A212: o,c // o,c1 by A27, A35, A36, A39, AFF_1:39, AFF_1:41;
A213: o,b // o,b1 by A26, A33, A34, A38, AFF_1:39, AFF_1:41;
then o,b1 // o,c by A29, A211, AFF_1:5;
then o,b1 // o,c1 by A30, A212, AFF_1:5;
then LIN o,b1,c1 by AFF_1:def 1;
then LIN b1,c1,o by AFF_1:6;
then b1,c1 // b1,o by AFF_1:def 1;
then b1,c1 // o,b1 by AFF_1:4;
then A214: o,b // b1,c1 by A74, A213, AFF_1:5;
LIN o,b,c by A211, AFF_1:def 1;
then LIN b,c,o by AFF_1:6;
then b,c // b,o by AFF_1:def 1;
then b,c // o,b by AFF_1:4;
hence contradiction by A29, A47, A214, AFF_1:5; :: thesis: verum

end;

A215: ( a <> b & a <> c )

proof

A216: now :: thesis: not a = c

assume a = c ; :: thesis: contradiction
then A217: o,a // M by A27, A35, A39, AFF_1:52;
o,a // Y by A25, A31, A37, AFF_1:52;
hence contradiction by A25, A27, A28, A41, A217, AFF_1:45, AFF_1:53; :: thesis: verum

end;

A218: now :: thesis: not a = b

assume a = b ; :: thesis: contradiction
then A219: o,a // Z by A26, A33, A38, AFF_1:52;
o,a // Y by A25, A31, A37, AFF_1:52;
hence contradiction by A25, A26, A28, A40, A219, AFF_1:45, AFF_1:53; :: thesis: verum

end;

assume ( not a <> b or not a <> c ) ; :: thesis: contradiction
hence contradiction by A218, A216; :: thesis: verum

end;

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

proof

A221: now :: thesis: not o in K

A222: o <> c1

proof

A223: a1 <> o

proof

A224: not LIN a,b,o

proof

assume LIN a,b,o ; :: thesis: contradiction
then LIN o,a,b by AFF_1:6;
then b in Y by A25, A28, A31, A37, AFF_1:25;
then A225: o,b // Y by A25, A37, AFF_1:52;
o,b // Z by A26, A33, A38, AFF_1:52;
hence contradiction by A25, A26, A29, A40, A225, AFF_1:45, AFF_1:53; :: thesis: verum

end;

A226: o,b // o,b1 by A26, A33, A34, A38, AFF_1:39, AFF_1:41;
assume a1 = o ; :: thesis: contradiction
then a,b // o,b by A42, A74, A226, AFF_1:5;
then b,a // b,o by AFF_1:4;
then LIN b,a,o by AFF_1:def 1;
then LIN o,a,b by AFF_1:6;
then o,a // o,b by AFF_1:def 1;
then o,a // o,b1 by A29, A226, AFF_1:5;
then LIN o,a,b1 by AFF_1:def 1;
then A227: LIN a,o,b1 by AFF_1:6;
b,o // b,b1 by A26, A33, A34, A38, AFF_1:39, AFF_1:41;
hence contradiction by A74, A224, A227, AFF_1:14; :: thesis: verum

end;

A228: not LIN c,a,o

proof

assume LIN c,a,o ; :: thesis: contradiction
then LIN o,a,c by AFF_1:6;
then c in Y by A25, A28, A31, A37, AFF_1:25;
then A229: o,c // Y by A25, A37, AFF_1:52;
o,c // M by A27, A35, A39, AFF_1:52;
hence contradiction by A25, A27, A30, A41, A229, AFF_1:45, AFF_1:53; :: thesis: verum

end;

A230: a1,o // o,a by A25, A31, A32, A37, AFF_1:39, AFF_1:41;
assume o = c1 ; :: thesis: contradiction
then a,c // o,a by A43, A223, A230, AFF_1:5;
then a,c // a,o by AFF_1:4;
then LIN a,c,o by AFF_1:def 1;
then LIN o,c,a by AFF_1:6;
then o,c // o,a by AFF_1:def 1;
then o,c // a1,o by A28, A230, AFF_1:5;
then o,c // o,a1 by AFF_1:4;
then LIN o,c,a1 by AFF_1:def 1;
then A231: LIN c,o,a1 by AFF_1:6;
a,o // a,a1 by A25, A31, A32, A37, AFF_1:39, AFF_1:41;
hence contradiction by A223, A228, A231, AFF_1:14; :: thesis: verum

end;

A232: o,c // o,c1 by A27, A35, A36, A39, AFF_1:39, AFF_1:41;
assume o in K ; :: thesis: contradiction
then A233: o,b1 // o,c1 by A153, A154, A155, AFF_1:39, AFF_1:41;
A234: o,b1 // o,b by A26, A33, A34, A38, AFF_1:39, AFF_1:41;
then o,b // o,c1 by A74, A233, AFF_1:5;
then o,b // o,c by A222, A232, AFF_1:5;
then LIN o,b,c by AFF_1:def 1;
then LIN b,c,o by AFF_1:6;
then b,c // b,o by AFF_1:def 1;
then b,c // o,b by AFF_1:4;
then b,c // o,b1 by A29, A234, AFF_1:5;
then A235: b,c // b1,o by AFF_1:4;
LIN o,b1,c1 by A233, AFF_1:def 1;
then LIN b1,c1,o by AFF_1:6;
then b1,c1 // b1,o by AFF_1:def 1;
hence contradiction by A47, A74, A235, AFF_1:5; :: thesis: verum

end;

A236: now :: thesis: not d1 in K

A237: d <> d1

proof

assume d = d1 ; :: thesis: contradiction
then A238: o,a // a,d by A85, A86, A87, A109, AFF_1:39, AFF_1:41;
o,a // a,a1 by A25, A31, A32, A37, AFF_1:39, AFF_1:41;
then a,a1 // a,d by A28, A238, AFF_1:5;
hence contradiction by A46, AFF_1:def 1; :: thesis: verum

end;

assume A239: d1 in K ; :: thesis: contradiction
c,c1 // c,o by A27, A35, A36, A39, AFF_1:39, AFF_1:41;
then A240: LIN c,c1,o by AFF_1:def 1;
A241: d,d1 // c1,c by A110, AFF_1:4;
d in K by A45, A159, A153, A154, A155, AFF_1:25;
then c in K by A153, A155, A239, A237, A241, AFF_1:48;
hence contradiction by A48, A153, A155, A221, A240, AFF_1:25; :: thesis: verum

end;

A242: now :: thesis: not a1 in K

assume a1 in K ; :: thesis: contradiction
then A243: a1,b1 // a1,c1 by A153, A154, A155, AFF_1:39, AFF_1:41;
then a,b // a1,c1 by A42, A75, AFF_1:5;
then a,b // a,c by A43, A75, 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 A244: b,c // a1,b1 by A42, A215, AFF_1:5;
LIN a1,b1,c1 by A243, AFF_1:def 1;
then LIN b1,c1,a1 by AFF_1:6;
then b1,c1 // b1,a1 by AFF_1:def 1;
then b1,c1 // a1,b1 by AFF_1:4;
hence contradiction by A47, A75, A244, AFF_1:5; :: thesis: verum

end;

A245: now :: thesis: not d2 in K

A246: d <> d2

proof

assume d = d2 ; :: thesis: contradiction
then A247: o,a // a,d by A85, A86, A87, A107, AFF_1:39, AFF_1:41;
o,a // a,a1 by A25, A31, A32, A37, AFF_1:39, AFF_1:41;
then a,a1 // a,d by A28, A247, AFF_1:5;
hence contradiction by A46, AFF_1:def 1; :: thesis: verum

end;

assume A248: d2 in K ; :: thesis: contradiction
d,d2 // a1,c1 by A43, A215, A108, AFF_1:5;
then A249: d,d2 // c1,a1 by AFF_1:4;
d in K by A45, A159, A153, A154, A155, AFF_1:25;
hence contradiction by A153, A155, A242, A248, A246, A249, AFF_1:48; :: thesis: verum

end;

assume ( o in K or a1 in K or d1 in K or d2 in K ) ; :: thesis: contradiction
hence contradiction by A221, A242, A236, A245; :: thesis: verum

end;

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

proof

A251: now :: thesis: not c1 in C

assume A252: c1 in C ; :: thesis: contradiction
o,c1 // c1,c by A27, A35, A36, A39, AFF_1:39, AFF_1:41;
hence contradiction by A155, A85, A86, A187, A220, A252, AFF_1:48; :: thesis: verum

end;

A253: now :: thesis: not d4 in C

assume A254: d4 in C ; :: thesis: contradiction
d1,d4 // d1,d3 by A186, AFF_1:4;
hence contradiction by A85, A109, A185, A187, A220, A254, AFF_1:48; :: thesis: verum

end;

A255: now :: thesis: not b1 in C

assume A256: b1 in C ; :: thesis: contradiction
o,b1 // o,b by A26, A33, A34, A38, AFF_1:39, AFF_1:41;
hence contradiction by A74, A85, A86, A187, A256, AFF_1:48; :: thesis: verum

end;

assume ( c1 in C or b1 in C or d in C or d4 in C ) ; :: thesis: contradiction
hence contradiction by A187, A251, A255, A253; :: thesis: verum

end;

a <> c

proof

assume a = c ; :: thesis: contradiction
then A257: o,a // M by A27, A35, A39, AFF_1:52;
o,a // Y by A25, A31, A37, AFF_1:52;
hence contradiction by A25, A27, A28, A41, A257, AFF_1:45, AFF_1:53; :: thesis: verum

end;

then a1,c1 // d,d2 by A43, A108, AFF_1:5;
then A258: a1,c1 // d2,d by AFF_1:4;
c1,o // c,c1 by A27, A35, A36, A39, AFF_1:39, AFF_1:41;
then A259: c1,o // d,d1 by A48, A110, AFF_1:5;
A260: d1 <> d2

proof

assume d1 = d2 ; :: thesis: contradiction
then a,c // c,c1 by A109, A110, A108, A187, AFF_1:5;
then c,c1 // c,a by AFF_1:4;
then LIN c,c1,a by AFF_1:def 1;
then a in M by A35, A36, A39, A48, AFF_1:25;
then A261: o,a // M by A27, A39, AFF_1:52;
o,a // Y by A25, A31, A37, AFF_1:52;
hence contradiction by A25, A27, A28, A41, A261, AFF_1:45, AFF_1:53; :: thesis: verum

end;

A262: not LIN d4,d2,d1

proof

assume LIN d4,d2,d1 ; :: thesis: contradiction
then LIN d1,d2,d4 by AFF_1:6;
hence contradiction by A85, A109, A107, A250, A260, AFF_1:25; :: thesis: verum

end;

A263: o,b // o,b1 by A26, A33, A34, A38, AFF_1:51;
a,c // d2,d by A108, AFF_1:4;
then a,b // d2,d3 by A24, A113, A114, A115, A85, A86, A87, A109, A107, A157, A158, A116, A129, A187, A111;
then A264: d2,d3 // a1,b1 by A42, A215, AFF_1:5;
o,b // d1,d4 by A109, A158, A186, A187, AFF_1:5;
then o,b1 // d1,d4 by A29, A263, AFF_1:5;
then a1,b1 // d2,d4 by A24, A153, A154, A155, A85, A86, A109, A107, A185, A112, A156, A220, A250, A258, A259;
then d2,d3 // d2,d4 by A75, A264, AFF_1:5;
then LIN d2,d3,d4 by AFF_1:def 1;
then LIN d4,d3,d2 by AFF_1:6;
then A265: d4,d3 // d4,d2 by AFF_1:def 1;
LIN d1,d3,d4 by A186, AFF_1:def 1;
then LIN d4,d3,d1 by AFF_1:6;
then d4,d3 // d4,d1 by AFF_1:def 1;
then d4,d2 // d4,d1 by A206, A265, AFF_1:5;
hence contradiction by A262, AFF_1:def 1; :: thesis: verum

end;

now :: thesis: not b1 = o

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

proof

A268: not LIN b,a,o

proof

assume LIN b,a,o ; :: thesis: contradiction
then LIN o,a,b by AFF_1:6;
then b in Y by A25, A28, A31, A37, AFF_1:25;
then A269: o,b // Y by A25, A37, AFF_1:52;
o,b // Z by A26, A33, A38, AFF_1:52;
hence contradiction by A25, A26, A29, A40, A269, AFF_1:45, AFF_1:53; :: thesis: verum

end;

A270: a1 <> a

proof

assume a1 = a ; :: thesis: contradiction
then LIN a,b,o by A42, A266, AFF_1:def 1;
then LIN o,a,b by AFF_1:6;
then b in Y by A25, A28, A31, A37, AFF_1:25;
then A271: o,b // Y by A25, A37, AFF_1:52;
o,b // Z by A26, A33, A38, AFF_1:52;
hence contradiction by A25, A26, A29, A40, A271, AFF_1:45, AFF_1:53; :: thesis: verum

end;

assume A272: o <> a1 ; :: thesis: contradiction
a1,o // a,a1 by A25, A31, A32, A37, AFF_1:51;
then a,b // a,a1 by A42, A266, A272, AFF_1:5;
then LIN a,b,a1 by AFF_1:def 1;
then LIN a1,b,a by AFF_1:6;
then A273: a1,b // a1,a by AFF_1:def 1;
a1,a // a1,o by A25, A31, A32, A37, AFF_1:51;
then a1,b // a1,o by A273, A270, AFF_1:5;
then LIN a1,b,o by AFF_1:def 1;
then LIN b,o,a1 by AFF_1:6;
hence contradiction by A25, A31, A32, A37, A272, A268, AFF_1:14, AFF_1:51; :: thesis: verum

end;

o = c1

proof

A274: not LIN a,c,o

proof

assume LIN a,c,o ; :: thesis: contradiction
then LIN o,a,c by AFF_1:6;
then c in Y by A25, A28, A31, A37, AFF_1:25;
then A275: o,c // Y by A25, A37, AFF_1:52;
o,c // M by A27, A35, A39, AFF_1:52;
hence contradiction by A25, A27, A30, A41, A275, AFF_1:45, AFF_1:53; :: thesis: verum

end;

assume A276: o <> c1 ; :: thesis: contradiction
A277: o,c1 // o,c by A27, A35, A36, A39, AFF_1:51;
then o,c // a,c by A43, A267, A276, AFF_1:5;
then c,o // c,a by AFF_1:4;
then LIN c,o,a by AFF_1:def 1;
then LIN o,a,c by AFF_1:6;
then o,a // o,c by AFF_1:def 1;
then o,a // o,c1 by A30, A277, AFF_1:5;
then LIN o,a,c1 by AFF_1:def 1;
then LIN a,o,c1 by AFF_1:6;
hence contradiction by A27, A35, A36, A39, A276, A274, AFF_1:14, AFF_1:51; :: thesis: verum

end;

hence contradiction by A47, A266, AFF_1:3; :: thesis: verum

end;

hence contradiction by A73; :: thesis: verum

end;

hence contradiction by A47, AFF_1:3; :: thesis: verum

end;

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

end;

A278: now :: thesis: Z // M

A279: M // M by A17, AFF_1:41;
consider d being Element of X such that
A280: LIN b,c,d and
A281: LIN b1,c1,d by A22, AFF_1:60;
A282: LIN a,a1,d by A2, A3, A4, A5, A6, A7, A8, A9, A10, A11, A12, A13, A14, A15, A16, A17, A18, A19, A20, A21, A22, A23, A280, A281;
A283: ( not a in Z & not a in M )

proof

A284: now :: thesis: not a in M

assume a in M ; :: thesis: contradiction
then A285: o,a // M by A5, A17, AFF_1:52;
o,a // Y by A3, A9, A15, AFF_1:52;
hence contradiction by A3, A5, A6, A19, A285, AFF_1:45, AFF_1:53; :: thesis: verum

end;

A286: now :: thesis: not a in Z

assume a in Z ; :: thesis: contradiction
then A287: o,a // Z by A4, A16, AFF_1:52;
o,a // Y by A3, A9, A15, AFF_1:52;
hence contradiction by A3, A4, A6, A18, A287, AFF_1:45, AFF_1:53; :: thesis: verum

end;

assume ( a in Z or a in M ) ; :: thesis: contradiction
hence contradiction by A286, A284; :: thesis: verum

end;

A288: ex d1 being Element of X st
( a,b // d,d1 & d1 in Z )

proof

consider e1 being Element of X such that
A289: o,b // o,e1 and
A290: o <> e1 by DIRAF:40;
consider e2 being Element of X such that
A291: a,b // d,e2 and
A292: d <> e2 by DIRAF:40;
not o,e1 // d,e2

proof

assume o,e1 // d,e2 ; :: thesis: contradiction
then o,b // d,e2 by A289, A290, AFF_1:5;
then o,b // a,b by A291, A292, AFF_1:5;
then b,o // b,a by AFF_1:4;
then LIN b,o,a by AFF_1:def 1;
hence contradiction by A4, A7, A11, A16, A283, AFF_1:25; :: thesis: verum

end;

then consider d1 being Element of X such that
A293: LIN o,e1,d1 and
A294: LIN d,e2,d1 by AFF_1:60;
o,e1 // o,d1 by A293, AFF_1:def 1;
then o,b // o,d1 by A289, A290, AFF_1:5;
then A295: LIN o,b,d1 by AFF_1:def 1;
take d1 ; :: thesis: ( a,b // d,d1 & d1 in Z )
d,e2 // d,d1 by A294, AFF_1:def 1;
hence ( a,b // d,d1 & d1 in Z ) by A4, A7, A11, A16, A291, A292, A295, AFF_1:5, AFF_1:25; :: thesis: verum

end;

A296: Z // Z by A16, AFF_1:41;
A297: ( a <> a1 & b <> b1 & c <> c1 )

proof

A298: now :: thesis: not a = a1

A299: not LIN a,o,b

proof

assume LIN a,o,b ; :: thesis: contradiction
then LIN o,b,a by AFF_1:6;
hence contradiction by A4, A7, A11, A16, A283, AFF_1:25; :: thesis: verum

end;

A300: not LIN a,o,c

proof

assume LIN a,o,c ; :: thesis: contradiction
then LIN o,c,a by AFF_1:6;
hence contradiction by A5, A8, A13, A17, A283, AFF_1:25; :: thesis: verum

end;

assume A301: a = a1 ; :: thesis: contradiction
then LIN a,c,c1 by A21, AFF_1:def 1;
then A302: c = c1 by A5, A13, A14, A279, A300, AFF_1:14, AFF_1:39;
LIN a,b,b1 by A20, A301, AFF_1:def 1;
then b = b1 by A4, A11, A12, A296, A299, AFF_1:14, AFF_1:39;
hence contradiction by A22, A302, AFF_1:2; :: thesis: verum

end;

A303: now :: thesis: not b = b1

assume b = b1 ; :: thesis: contradiction
then b,a // b,a1 by A20, AFF_1:4;
then A304: LIN b,a,a1 by AFF_1:def 1;
o,a // o,a1 by A3, A9, A10, A15, AFF_1:39, AFF_1:41;
hence contradiction by A4, A7, A11, A16, A283, A298, A304, AFF_1:14, AFF_1:25; :: thesis: verum

end;

A305: now :: thesis: not c = c1

assume c = c1 ; :: thesis: contradiction
then c,a // c,a1 by A21, AFF_1:4;
then A306: LIN c,a,a1 by AFF_1:def 1;
o,a // o,a1 by A3, A9, A10, A15, AFF_1:39, AFF_1:41;
hence contradiction by A5, A8, A13, A17, A283, A298, A306, AFF_1:14, AFF_1:25; :: thesis: verum

end;

assume ( not a <> a1 or not b <> b1 or not c <> c1 ) ; :: thesis: contradiction
hence contradiction by A298, A303, A305; :: thesis: verum

end;

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

proof

A308: now :: thesis: not a1 = o

assume A309: a1 = o ; :: thesis: contradiction
A310: o = c1

proof

A311: not LIN c,a,o

proof

assume LIN c,a,o ; :: thesis: contradiction
then LIN o,c,a by AFF_1:6;
hence contradiction by A5, A8, A13, A17, A283, AFF_1:25; :: thesis: verum

end;

assume A312: o <> c1 ; :: thesis: contradiction
A313: o,c1 // o,c by A5, A13, A14, A17, AFF_1:39, AFF_1:41;
then a,c // o,c by A21, A309, A312, AFF_1:5;
then c,o // c,a by AFF_1:4;
then LIN c,o,a by AFF_1:def 1;
then LIN o,c,a by AFF_1:6;
then o,c // o,a by AFF_1:def 1;
then o,c1 // o,a by A8, A313, AFF_1:5;
then LIN o,c1,a by AFF_1:def 1;
then LIN a,o,c1 by AFF_1:6;
then A314: a,o // a,c1 by AFF_1:def 1;
c,o // c,c1 by A5, A13, A14, A17, AFF_1:39, AFF_1:41;
then LIN c,o,c1 by AFF_1:def 1;
hence contradiction by A312, A311, A314, AFF_1:14; :: thesis: verum

end;

o = b1

proof

A315: not LIN b,a,o

proof

assume LIN b,a,o ; :: thesis: contradiction
then LIN o,b,a by AFF_1:6;
hence contradiction by A4, A7, A11, A16, A283, AFF_1:25; :: thesis: verum

end;

assume A316: o <> b1 ; :: thesis: contradiction
A317: o,b1 // o,b by A4, A11, A12, A16, AFF_1:39, AFF_1:41;
then a,b // o,b by A20, A309, A316, AFF_1:5;
then b,a // b,o by AFF_1:4;
then LIN b,a,o by AFF_1:def 1;
then LIN o,a,b by AFF_1:6;
then o,a // o,b by AFF_1:def 1;
then o,a // o,b1 by A7, A317, AFF_1:5;
then LIN o,a,b1 by AFF_1:def 1;
then LIN a,o,b1 by AFF_1:6;
then A318: a,o // a,b1 by AFF_1:def 1;
b,o // b,b1 by A4, A11, A12, A16, AFF_1:39, AFF_1:41;
then LIN b,o,b1 by AFF_1:def 1;
hence contradiction by A316, A315, A318, AFF_1:14; :: thesis: verum

end;

hence contradiction by A22, A310, AFF_1:3; :: thesis: verum

end;

A319: now :: thesis: not b1 = o

A320: not LIN a,b,o

proof

assume LIN a,b,o ; :: thesis: contradiction
then LIN o,b,a by AFF_1:6;
hence contradiction by A4, A7, A11, A16, A283, AFF_1:25; :: thesis: verum

end;

A321: a1,o // a,a1 by A3, A9, A10, A15, AFF_1:39, AFF_1:41;
assume b1 = o ; :: thesis: contradiction
then a,b // a,a1 by A20, A308, A321, AFF_1:5;
then LIN a,b,a1 by AFF_1:def 1;
then LIN a1,b,a by AFF_1:6;
then a1,b // a1,a by AFF_1:def 1;
then a1,b // a,a1 by AFF_1:4;
then a1,b // a1,o by A297, A321, AFF_1:5;
then LIN a1,b,o by AFF_1:def 1;
then LIN b,o,a1 by AFF_1:6;
then A322: b,o // b,a1 by AFF_1:def 1;
a,o // a,a1 by A3, A9, A10, A15, AFF_1:39, AFF_1:41;
then LIN a,o,a1 by AFF_1:def 1;
hence contradiction by A308, A320, A322, AFF_1:14; :: thesis: verum

end;

A323: now :: thesis: not c1 = o

A324: not LIN a,c,o

proof

assume LIN a,c,o ; :: thesis: contradiction
then LIN o,c,a by AFF_1:6;
hence contradiction by A5, A8, A13, A17, A283, AFF_1:25; :: thesis: verum

end;

A325: a1,o // a,a1 by A3, A9, A10, A15, AFF_1:39, AFF_1:41;
assume c1 = o ; :: thesis: contradiction
then a,c // a,a1 by A21, A308, A325, AFF_1:5;
then LIN a,c,a1 by AFF_1:def 1;
then LIN a1,a,c by AFF_1:6;
then a1,a // a1,c by AFF_1:def 1;
then a,a1 // a1,c by AFF_1:4;
then a1,o // a1,c by A297, A325, AFF_1:5;
then LIN a1,o,c by AFF_1:def 1;
then LIN c,o,a1 by AFF_1:6;
then A326: c,o // c,a1 by AFF_1:def 1;
a,o // a,a1 by A3, A9, A10, A15, AFF_1:39, AFF_1:41;
then LIN a,o,a1 by AFF_1:def 1;
hence contradiction by A308, A324, A326, AFF_1:14; :: thesis: verum

end;

assume ( not a1 <> o or not b1 <> o or not c1 <> o ) ; :: thesis: contradiction
hence contradiction by A308, A319, A323; :: thesis: verum

end;

ex d2 being Element of X st
( a,c // d,d2 & d2 in M )

proof

consider e1 being Element of X such that
A327: o,c // o,e1 and
A328: o <> e1 by DIRAF:40;
consider e2 being Element of X such that
A329: a,c // d,e2 and
A330: d <> e2 by DIRAF:40;
not o,e1 // d,e2

proof

assume o,e1 // d,e2 ; :: thesis: contradiction
then o,c // d,e2 by A327, A328, AFF_1:5;
then o,c // a,c by A329, A330, AFF_1:5;
then c,o // c,a by AFF_1:4;
then LIN c,o,a by AFF_1:def 1;
hence contradiction by A5, A8, A13, A17, A283, AFF_1:25; :: thesis: verum

end;

then consider d2 being Element of X such that
A331: LIN o,e1,d2 and
A332: LIN d,e2,d2 by AFF_1:60;
o,e1 // o,d2 by A331, AFF_1:def 1;
then o,c // o,d2 by A327, A328, AFF_1:5;
then A333: LIN o,c,d2 by AFF_1:def 1;
take d2 ; :: thesis: ( a,c // d,d2 & d2 in M )
d,e2 // d,d2 by A332, AFF_1:def 1;
hence ( a,c // d,d2 & d2 in M ) by A5, A8, A13, A17, A329, A330, A333, AFF_1:5, AFF_1:25; :: thesis: verum

end;

then consider d2 being Element of X such that
A334: a,c // d,d2 and
A335: d2 in M ;
consider d1 being Element of X such that
A336: a,b // d,d1 and
A337: d1 in Z by A288;
assume A338: not Z // M ; :: thesis: contradiction
A339: d1 <> d2

proof

A340: o <> d1

proof

A341: o <> d

proof

assume o = d ; :: thesis: contradiction
then LIN o,b,c by A280, AFF_1:6;
then c in Z by A4, A7, A11, A16, AFF_1:25;
then A342: o,c // Z by A4, A16, AFF_1:52;
o,c // M by A5, A13, A17, AFF_1:52;
hence contradiction by A8, A338, A342, AFF_1:53; :: thesis: verum

end;

A343: a,a1 // a,d by A282, AFF_1:def 1;
a,o // a,a1 by A3, A9, A10, A15, AFF_1:39, AFF_1:41;
then a,o // a,d by A297, A343, AFF_1:5;
then LIN a,o,d by AFF_1:def 1;
then LIN o,a,d by AFF_1:6;
then o,a // o,d by AFF_1:def 1;
then A344: a,o // d,o by AFF_1:4;
assume o = d1 ; :: thesis: contradiction
then a,b // a,o by A336, A341, A344, AFF_1:5;
then LIN a,b,o by AFF_1:def 1;
then LIN o,b,a by AFF_1:6;
hence contradiction by A4, A7, A11, A16, A283, AFF_1:25; :: thesis: verum

end;

assume d1 = d2 ; :: thesis: contradiction
then A345: o,d1 // M by A5, A17, A335, AFF_1:52;
o,d1 // Z by A4, A16, A337, AFF_1:52;
hence contradiction by A338, A345, A340, AFF_1:53; :: thesis: verum

end;

A346: now :: thesis: not b1,c1 // d1,d2

assume A347: 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
A348: b,c // b,e1 and
A349: b <> e1 by DIRAF:40;
consider e2 being Element of X such that
A350: d1,d2 // d1,e2 and
A351: d1 <> e2 by DIRAF:40;
not b,e1 // d1,e2

proof

assume b,e1 // d1,e2 ; :: thesis: contradiction
then b,e1 // d1,d2 by A350, A351, AFF_1:5;
then b,c // d1,d2 by A348, A349, AFF_1:5;
hence contradiction by A22, A339, A347, AFF_1:5; :: thesis: verum

end;

then consider d5 being Element of X such that
A352: LIN b,e1,d5 and
A353: LIN d1,e2,d5 by AFF_1:60;
b,e1 // b,d5 by A352, AFF_1:def 1;
then A354: b,c // b,d5 by A348, A349, AFF_1:5;
take d5 ; :: thesis: ( LIN b,c,d5 & LIN d1,d2,d5 )
d1,e2 // d1,d5 by A353, AFF_1:def 1;
then d1,d2 // d1,d5 by A350, A351, AFF_1:5;
hence ( LIN b,c,d5 & LIN d1,d2,d5 ) by A354, AFF_1:def 1; :: thesis: verum

end;

then consider d5 being Element of X such that
A355: LIN b,c,d5 and
A356: LIN d1,d2,d5 ;
A357: d in Y by A9, A10, A15, A297, A282, AFF_1:25;

A358: now :: thesis: not LIN a,d,d5

A359: not LIN a,b,d

proof

A360: a <> d

proof

A361: a1 <> b1

proof

o,a1 // o,a by A3, A9, A10, A15, AFF_1:39, AFF_1:41;
then A362: LIN o,a1,a by AFF_1:def 1;
assume a1 = b1 ; :: thesis: contradiction
hence contradiction by A4, A12, A16, A283, A307, A362, AFF_1:25; :: thesis: verum

end;

assume A363: a = d ; :: thesis: contradiction
then LIN a,b,c by A280, AFF_1:6;
then a,b // a,c by AFF_1:def 1;
then a1,b1 // a,c by A11, A20, A283, AFF_1:5;
then a1,b1 // a1,c1 by A13, A21, A283, AFF_1:5;
then LIN a1,b1,c1 by AFF_1:def 1;
then LIN b1,c1,a1 by AFF_1:6;
then b1,c1 // b1,a1 by AFF_1:def 1;
then A364: b1,c1 // a1,b1 by AFF_1:4;
b,c // b,a by A280, A363, AFF_1:def 1;
then b,c // a,b by AFF_1:4;
then b,c // a1,b1 by A11, A20, A283, AFF_1:5;
hence contradiction by A22, A364, A361, AFF_1:5; :: thesis: verum

end;

assume LIN a,b,d ; :: thesis: contradiction
then LIN a,d,b by AFF_1:6;
then b in Y by A9, A15, A357, A360, AFF_1:25;
then A365: o,b // Y by A3, A15, AFF_1:52;
o,b // Z by A4, A11, A16, AFF_1:52;
hence contradiction by A3, A4, A7, A18, A365, AFF_1:45, AFF_1:53; :: thesis: verum

end;

assume A366: LIN a,d,d5 ; :: thesis: contradiction
A367: o <> d

proof

A368: o,b // o,b1 by A4, A11, A12, A16, AFF_1:39, AFF_1:41;
assume A369: o = d ; :: thesis: contradiction
then LIN o,b,c by A280, AFF_1:6;
then o,b // o,c by AFF_1:def 1;
then A370: o,b1 // o,c by A7, A368, AFF_1:5;
o,c // o,c1 by A5, A13, A14, A17, AFF_1:39, AFF_1:41;
then o,b1 // o,c1 by A8, A370, AFF_1:5;
then LIN o,b1,c1 by AFF_1:def 1;
then LIN b1,c1,o by AFF_1:6;
then b1,c1 // b1,o by AFF_1:def 1;
then A371: b1,c1 // o,b1 by AFF_1:4;
b,c // b,o by A280, A369, AFF_1:def 1;
then b,c // o,b by AFF_1:4;
then b,c // o,b1 by A7, A368, AFF_1:5;
hence contradiction by A22, A307, A371, AFF_1:5; :: thesis: verum

end;

A372: d <> d1

proof

assume d = d1 ; :: thesis: contradiction
then A373: o,d // Z by A4, A16, A337, AFF_1:52;
o,d // Y by A3, A15, A357, AFF_1:52;
hence contradiction by A3, A4, A18, A367, A373, AFF_1:45, AFF_1:53; :: thesis: verum

end;

A374: d <> d2

proof

assume d = d2 ; :: thesis: contradiction
then A375: o,d // M by A5, A17, A335, AFF_1:52;
o,d // Y by A3, A15, A357, AFF_1:52;
hence contradiction by A3, A5, A19, A367, A375, AFF_1:45, AFF_1:53; :: thesis: verum

end;

A376: b,c // b,d5 by A355, AFF_1:def 1;
A377: b,c // b,d by A280, AFF_1:def 1;
b <> c by A22, AFF_1:3;
then b,d // b,d5 by A377, A376, AFF_1:5;
then LIN d1,d2,d by A356, A366, A359, AFF_1:14;
then LIN d,d1,d2 by AFF_1:6;
then d,d1 // d,d2 by AFF_1:def 1;
then a,b // d,d2 by A336, A372, AFF_1:5;
then A378: a,b // a,c by A334, A374, 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 A379: b,c // a1,b1 by A11, A20, A283, AFF_1:5;
a1,b1 // a,c by A11, A20, A283, A378, AFF_1:5;
then a1,b1 // a1,c1 by A13, A21, A283, AFF_1:5;
then LIN a1,b1,c1 by AFF_1:def 1;
then LIN b1,c1,a1 by AFF_1:6;
then b1,c1 // b1,a1 by AFF_1:def 1;
then A380: b1,c1 // a1,b1 by AFF_1:4;
a1 <> b1

proof

o,a1 // o,a by A3, A9, A10, A15, AFF_1:39, AFF_1:41;
then A381: LIN o,a1,a by AFF_1:def 1;
assume a1 = b1 ; :: thesis: contradiction
hence contradiction by A4, A12, A16, A283, A307, A381, AFF_1:25; :: thesis: verum

end;

hence contradiction by A22, A380, A379, AFF_1:5; :: thesis: verum

end;

not b,c // d1,d2 by A22, A339, A347, AFF_1:5;
hence contradiction by A2, A3, A4, A5, A6, A7, A8, A9, A11, A13, A15, A16, A17, A18, A19, A23, A336, A337, A334, A335, A355, A356, A357, A358; :: thesis: verum

end;

now :: thesis: b1,c1 // d1,d2

A382: d in Y by A9, A10, A15, A297, A282, AFF_1:25;
A383: not LIN a1,b1,d

proof

A384: a1 <> d

proof

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

proof

o,a1 // o,a by A3, A9, A10, A15, AFF_1:39, AFF_1:41;
then A386: LIN o,a1,a by AFF_1:def 1;
assume ( not a1 <> b1 or not a1 <> c1 ) ; :: thesis: contradiction
hence contradiction by A4, A5, A12, A14, A16, A17, A283, A307, A386, AFF_1:25; :: thesis: verum

end;

assume A387: a1 = d ; :: thesis: contradiction
then LIN a1,b1,c1 by A281, AFF_1:6;
then a1,b1 // a1,c1 by AFF_1:def 1;
then a,b // a1,c1 by A20, A385, AFF_1:5;
then a,b // a,c by A21, A385, 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 A388: b,c // a,b by AFF_1:4;
b1,c1 // b1,a1 by A281, A387, AFF_1:def 1;
then b1,c1 // a1,b1 by AFF_1:4;
then b1,c1 // a,b by A20, A385, AFF_1:5;
hence contradiction by A11, A22, A283, A388, AFF_1:5; :: thesis: verum

end;

assume LIN a1,b1,d ; :: thesis: contradiction
then LIN a1,d,b1 by AFF_1:6;
then b1 in Y by A10, A15, A382, A384, AFF_1:25;
then o,b1 // o,a by A3, A9, A15, AFF_1:39, AFF_1:41;
then LIN o,b1,a by AFF_1:def 1;
hence contradiction by A4, A12, A16, A283, A307, AFF_1:25; :: thesis: verum

end;

A389: d <> o

proof

A390: o,b // o,b1 by A4, A11, A12, A16, AFF_1:39, AFF_1:41;
assume A391: d = o ; :: thesis: contradiction
then LIN o,b,c by A280, AFF_1:6;
then o,b // o,c by AFF_1:def 1;
then A392: o,b1 // o,c by A7, A390, AFF_1:5;
o,c // o,c1 by A5, A13, A14, A17, AFF_1:39, AFF_1:41;
then o,b1 // o,c1 by A8, A392, AFF_1:5;
then LIN o,b1,c1 by AFF_1:def 1;
then LIN b1,c1,o by AFF_1:6;
then b1,c1 // b1,o by AFF_1:def 1;
then A393: b1,c1 // o,b1 by AFF_1:4;
b,c // b,o by A280, A391, AFF_1:def 1;
then b,c // o,b by AFF_1:4;
then b,c // o,b1 by A7, A390, AFF_1:5;
hence contradiction by A22, A307, A393, AFF_1:5; :: thesis: verum

end;

A394: d <> d1

proof

o,d // o,a by A3, A9, A15, A382, AFF_1:39, AFF_1:41;
then A395: LIN o,d,a by AFF_1:def 1;
assume d = d1 ; :: thesis: contradiction
hence contradiction by A4, A16, A283, A337, A389, A395, AFF_1:25; :: thesis: verum

end;

A396: d <> d2

proof

o,d // o,a by A3, A9, A15, A382, AFF_1:39, AFF_1:41;
then A397: LIN o,d,a by AFF_1:def 1;
assume d = d2 ; :: thesis: contradiction
hence contradiction by A5, A17, A283, A335, A389, A397, AFF_1:25; :: thesis: verum

end;

A398: a1,c1 // d,d2 by A13, A21, A283, A334, AFF_1:5;
A399: b1 <> c1 by A22, AFF_1:3;
A400: b1,c1 // b1,d by A281, AFF_1:def 1;
assume A401: not b1,c1 // d1,d2 ; :: thesis: contradiction
then consider d5 being Element of X such that
A402: LIN b1,c1,d5 and
A403: LIN d1,d2,d5 by AFF_1:60;
b1,c1 // b1,d5 by A402, AFF_1:def 1;
then A404: b1,d // b1,d5 by A399, A400, AFF_1:5;
a1,b1 // d,d1 by A11, A20, A283, A336, AFF_1:5;
then LIN a1,d,d5 by A2, A3, A4, A5, A10, A12, A14, A15, A16, A17, A18, A19, A23, A307, A337, A335, A401, A402, A403, A382, A398;
then d = d5 by A383, A404, AFF_1:14;
then LIN d,d1,d2 by A403, AFF_1:6;
then d,d1 // d,d2 by AFF_1:def 1;
then a,b // d,d2 by A336, A394, AFF_1:5;
then A405: a,b // a,c by A334, A396, 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 A406: b,c // a1,b1 by A11, A20, A283, AFF_1:5;
a1,b1 // a,c by A11, A20, A283, A405, AFF_1:5;
then a1,b1 // a1,c1 by A13, A21, A283, AFF_1:5;
then LIN a1,b1,c1 by AFF_1:def 1;
then LIN b1,c1,a1 by AFF_1:6;
then b1,c1 // b1,a1 by AFF_1:def 1;
then A407: b1,c1 // a1,b1 by AFF_1:4;
a1 <> b1

proof

o,a1 // o,a by A3, A9, A10, A15, AFF_1:39, AFF_1:41;
then A408: LIN o,a1,a by AFF_1:def 1;
assume a1 = b1 ; :: thesis: contradiction
hence contradiction by A4, A12, A16, A283, A307, A408, AFF_1:25; :: thesis: verum

end;

hence contradiction by A22, A407, A406, AFF_1:5; :: thesis: verum

end;

hence contradiction by A346; :: thesis: verum

end;

now :: thesis: not Z // M

assume A409: Z // M ; :: thesis: contradiction
then A410: b1 in M by A4, A5, A12, AFF_1:45;
b in M by A4, A5, A11, A409, AFF_1:45;
hence contradiction by A13, A14, A17, A22, A410, AFF_1:39, AFF_1:41; :: thesis: verum

end;

hence contradiction by A278; :: 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 A411: X is Desarguesian ; :: thesis: X is satisfying_Scherungssatz
then X is satisfying_TDES_1 by AFF_2:3, AFF_2:12;
then X is satisfying_des_1 by AFF_2:13;
then X is translational by AFF_2:7;
then A412: X is satisfying_minor_Scherungssatz by Th6;
X is satisfying_major_Scherungssatz by A411, Th7;
hence X is satisfying_Scherungssatz by A412, Th2; :: thesis: verum

end;

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