let X be AffinPlane; ( X is Desarguesian iff X is satisfying_Scherungssatz )
A1:
( X is satisfying_Scherungssatz implies X is Desarguesian )
proof
assume A2:
X is
satisfying_Scherungssatz
;
X is Desarguesian
now 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,c1let Y,
Z,
M be
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,c1let o,
a,
b,
c,
a1,
b1,
c1 be
Element of
X;
( 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
;
b,c // b1,c1assume A22:
not
b,
c // b1,
c1
;
contradictionA23:
now 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,c1let Y,
Z,
M be
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,c1let o,
a,
b,
c,
a1,
b1,
c1,
d be
Element of
X;
( 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
;
( 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
;
( 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
;
contradiction
A48:
(
c <> c1 &
a <> a1 &
b <> b1 )
proof
A49:
now not b = b1A50:
not
LIN o,
a,
c
proof
assume
LIN o,
a,
c
;
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;
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
;
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;
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
;
contradictionthen
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;
verum end;
A57:
now not c = c1A58:
not
LIN o,
a,
b
proof
assume
LIN o,
a,
b
;
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;
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
;
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;
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
;
contradictionthen
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;
verum end;
A65:
now not a = a1A66:
not
LIN o,
a,
c
proof
assume
LIN o,
a,
c
;
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;
verum
end; A68:
not
LIN o,
a,
b
proof
assume
LIN o,
a,
b
;
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;
verum
end; assume A70:
a = a1
;
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;
verum end;
assume
( not
c <> c1 or not
a <> a1 or not
b <> b1 )
;
contradiction
hence
contradiction
by A57, A65, A49;
verum
end;
now not b <> cassume A72:
b <> c
;
contradictionA73:
now not b1 <> oassume A74:
b1 <> o
;
contradictionA75:
(
a1 <> b1 &
a1 <> c1 )
proof
A76:
now not a1 = c1A77:
o <> a1
proof
A78:
not
LIN a,
b,
o
proof
assume
LIN a,
b,
o
;
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;
verum
end;
A80:
o,
b // o,
b1
by A26, A33, A34, A38, AFF_1:39, AFF_1:41;
assume
o = a1
;
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;
verum
end; assume
a1 = c1
;
contradictionthen 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;
verum end;
A83:
now not a1 = b1assume
a1 = b1
;
contradictionthen 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;
verum end;
assume
( not
a1 <> b1 or not
a1 <> c1 )
;
contradiction
hence
contradiction
by A83, A76;
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
;
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;
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
;
( 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;
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
;
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;
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
;
( 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;
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
;
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;
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
;
( 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;
verum
end; A129:
( not
o in A & not
a in A & not
d1 in A & not
d2 in A )
proof
A130:
now not a in AA131:
a <> b
proof
assume
a = b
;
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;
verum
end; A133:
a1 <> b1
proof
assume
a1 = b1
;
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;
verum
end; assume
a in A
;
contradictionthen A135:
a,
b // a,
c
by A113, A114, A115, AFF_1:39, AFF_1:41;
a <> c
proof
assume
a = c
;
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;
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;
verum end;
A138:
now not d2 in AA139:
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
;
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;
verum
end; assume A141:
d2 in A
;
contradictionA142:
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;
verum end;
A143:
now not o in Aassume
o in A
;
contradictionthen 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;
verum end;
A147:
now not d1 in AA148:
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
;
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;
verum
end; assume A150:
d1 in A
;
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;
verum end;
assume
(
o in A or
a in A or
d1 in A or
d2 in A )
;
contradiction
hence
contradiction
by A143, A130, A147, A138;
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
;
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;
verum
end;
assume A168:
o = c1
;
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;
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
;
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;
verum
end;
assume A174:
d1 = d3
;
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;
verum
end;
assume
b1,
e1 // d1,
e2
;
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;
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
;
( 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;
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 not b in Cassume
b in C
;
contradictionthen
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;
verum end;
A190:
now not d3 in CA191:
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
;
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;
verum
end;
assume A194:
d1 = d3
;
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;
verum
end; assume A201:
d3 in C
;
contradiction
d1,
d3 // o,
b
by A158, AFF_1:4;
hence
contradiction
by A85, A86, A109, A188, A201, A191, AFF_1:48;
verum end;
A202:
now not c in Cassume
c in C
;
contradictionthen
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;
verum end;
A204:
now not d in Cassume
d in C
;
contradictionthen 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;
verum end;
assume
(
c in C or
b in C or
d in C or
d3 in C )
;
contradiction
hence
contradiction
by A202, A188, A204, A190;
verum
end; A206:
d4 <> d3
proof
assume A207:
d4 = d3
;
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
;
contradiction
hence
contradiction
by A47, A209, A208, AFF_1:5;
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;
verum
end; A215:
(
a <> b &
a <> c )
proof
A216:
now not a = cassume
a = c
;
contradictionthen 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;
verum end;
A218:
now not a = bassume
a = b
;
contradictionthen 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;
verum end;
assume
( not
a <> b or not
a <> c )
;
contradiction
hence
contradiction
by A218, A216;
verum
end; A220:
( not
o in K & not
a1 in K & not
d1 in K & not
d2 in K )
proof
A221:
now not o in KA222:
o <> c1
proof
A223:
a1 <> o
proof
A224:
not
LIN a,
b,
o
proof
assume
LIN a,
b,
o
;
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;
verum
end;
A226:
o,
b // o,
b1
by A26, A33, A34, A38, AFF_1:39, AFF_1:41;
assume
a1 = o
;
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;
verum
end;
A228:
not
LIN c,
a,
o
proof
assume
LIN c,
a,
o
;
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;
verum
end;
A230:
a1,
o // o,
a
by A25, A31, A32, A37, AFF_1:39, AFF_1:41;
assume
o = c1
;
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;
verum
end; A232:
o,
c // o,
c1
by A27, A35, A36, A39, AFF_1:39, AFF_1:41;
assume
o in K
;
contradictionthen 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;
verum end;
A236:
now not d1 in KA237:
d <> d1
proof
assume
d = d1
;
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;
verum
end; assume A239:
d1 in K
;
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;
verum end;
A242:
now not a1 in Kassume
a1 in K
;
contradictionthen 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;
verum end;
A245:
now not d2 in KA246:
d <> d2
proof
assume
d = d2
;
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;
verum
end; assume A248:
d2 in K
;
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;
verum end;
assume
(
o in K or
a1 in K or
d1 in K or
d2 in K )
;
contradiction
hence
contradiction
by A221, A242, A236, A245;
verum
end; A250:
( not
c1 in C & not
b1 in C & not
d in C & not
d4 in C )
proof
A251:
now not c1 in Cassume A252:
c1 in C
;
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;
verum end;
A253:
now not d4 in Cend;
A255:
now not b1 in Cassume A256:
b1 in C
;
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;
verum end;
assume
(
c1 in C or
b1 in C or
d in C or
d4 in C )
;
contradiction
hence
contradiction
by A187, A251, A255, A253;
verum
end;
a <> c
proof
assume
a = c
;
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;
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
;
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;
verum
end; A262:
not
LIN d4,
d2,
d1
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;
verum end; now not b1 = oassume A266:
b1 = o
;
contradictionA267:
o = a1
proof
A268:
not
LIN b,
a,
o
proof
assume
LIN b,
a,
o
;
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;
verum
end;
A270:
a1 <> a
proof
assume
a1 = a
;
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;
verum
end;
assume A272:
o <> a1
;
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;
verum
end;
o = c1
proof
A274:
not
LIN a,
c,
o
proof
assume
LIN a,
c,
o
;
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;
verum
end;
assume A276:
o <> c1
;
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;
verum
end; hence
contradiction
by A47, A266, AFF_1:3;
verum end; hence
contradiction
by A73;
verum end;
hence
contradiction
by A47, AFF_1:3;
verum
end; hence
(
LIN a,
a1,
d or
b,
c // b1,
c1 )
;
verum end; A278:
now Z // MA279:
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 not a in Massume
a in M
;
contradictionthen 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;
verum end;
A286:
now not a in Zassume
a in Z
;
contradictionthen 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;
verum end;
assume
(
a in Z or
a in M )
;
contradiction
hence
contradiction
by A286, A284;
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
;
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;
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
;
( 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;
verum
end; A296:
Z // Z
by A16, AFF_1:41;
A297:
(
a <> a1 &
b <> b1 &
c <> c1 )
proof
A298:
now not a = a1A299:
not
LIN a,
o,
b
A300:
not
LIN a,
o,
c
assume A301:
a = a1
;
contradictionthen
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;
verum end;
A303:
now not b = b1assume
b = b1
;
contradictionthen
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;
verum end;
A305:
now not c = c1assume
c = c1
;
contradictionthen
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;
verum end;
assume
( not
a <> a1 or not
b <> b1 or not
c <> c1 )
;
contradiction
hence
contradiction
by A298, A303, A305;
verum
end; A307:
(
a1 <> o &
b1 <> o &
c1 <> o )
proof
A308:
now not a1 = oassume A309:
a1 = o
;
contradictionA310:
o = c1
proof
A311:
not
LIN c,
a,
o
assume A312:
o <> c1
;
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;
verum
end;
o = b1
proof
A315:
not
LIN b,
a,
o
assume A316:
o <> b1
;
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;
verum
end; hence
contradiction
by A22, A310, AFF_1:3;
verum end;
A319:
now not b1 = oA320:
not
LIN a,
b,
o
A321:
a1,
o // a,
a1
by A3, A9, A10, A15, AFF_1:39, AFF_1:41;
assume
b1 = o
;
contradictionthen
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;
verum end;
A323:
now not c1 = oA324:
not
LIN a,
c,
o
A325:
a1,
o // a,
a1
by A3, A9, A10, A15, AFF_1:39, AFF_1:41;
assume
c1 = o
;
contradictionthen
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;
verum end;
assume
( not
a1 <> o or not
b1 <> o or not
c1 <> o )
;
contradiction
hence
contradiction
by A308, A319, A323;
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
;
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;
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
;
( 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;
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
;
contradictionA339:
d1 <> d2
proof
A340:
o <> d1
proof
A341:
o <> d
proof
assume
o = d
;
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;
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
;
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;
verum
end;
assume
d1 = d2
;
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;
verum
end; A346:
now not b1,c1 // d1,d2assume A347:
b1,
c1 // d1,
d2
;
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
;
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;
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
;
( 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;
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 not LIN a,d,d5A359:
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
;
contradiction
hence
contradiction
by A4, A12, A16, A283, A307, A362, AFF_1:25;
verum
end;
assume A363:
a = d
;
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;
verum
end;
assume
LIN a,
b,
d
;
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;
verum
end; assume A366:
LIN a,
d,
d5
;
contradictionA367:
o <> d
proof
A368:
o,
b // o,
b1
by A4, A11, A12, A16, AFF_1:39, AFF_1:41;
assume A369:
o = d
;
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;
verum
end; A372:
d <> d1
proof
assume
d = d1
;
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;
verum
end; A374:
d <> d2
proof
assume
d = d2
;
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;
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
;
contradiction
hence
contradiction
by A4, A12, A16, A283, A307, A381, AFF_1:25;
verum
end; hence
contradiction
by A22, A380, A379, AFF_1:5;
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;
verum end; now b1,c1 // d1,d2A382:
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 )
;
contradiction
hence
contradiction
by A4, A5, A12, A14, A16, A17, A283, A307, A386, AFF_1:25;
verum
end;
assume A387:
a1 = d
;
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;
verum
end;
assume
LIN a1,
b1,
d
;
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;
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
;
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;
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
;
contradiction
hence
contradiction
by A4, A16, A283, A337, A389, A395, AFF_1:25;
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
;
contradiction
hence
contradiction
by A5, A17, A283, A335, A389, A397, AFF_1:25;
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
;
contradictionthen 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
;
contradiction
hence
contradiction
by A4, A12, A16, A283, A307, A408, AFF_1:25;
verum
end; hence
contradiction
by A22, A407, A406, AFF_1:5;
verum end; hence
contradiction
by A346;
verum end; now not Z // Massume A409:
Z // M
;
contradictionthen 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;
verum end; hence
contradiction
by A278;
verum end;
hence
X is
Desarguesian
by AFF_2:def 4;
verum
end;
( X is Desarguesian implies X is satisfying_Scherungssatz )
hence
( X is Desarguesian iff X is satisfying_Scherungssatz )
by A1; verum