let X be OrtAfPl; ( X is satisfying_OPAP & X is satisfying_DES implies X is satisfying_PAP )
assume that
A1:
X is satisfying_OPAP
and
A2:
X is satisfying_DES
; X is satisfying_PAP
let o be Element of X; CONMETR:def 2 for a1, a2, a3, b1, b2, b3 being Element of X
for M, N being Subset of X st M is being_line & N is being_line & o in M & a1 in M & a2 in M & a3 in M & o in N & b1 in N & b2 in N & b3 in N & not b2 in M & not a3 in N & o <> a1 & o <> a2 & o <> a3 & o <> b1 & o <> b2 & o <> b3 & a3,b2 // a2,b1 & a3,b3 // a1,b1 holds
a1,b2 // a2,b3
let a1, a2, a3, b1, b2, b3 be Element of X; for M, N being Subset of X st M is being_line & N is being_line & o in M & a1 in M & a2 in M & a3 in M & o in N & b1 in N & b2 in N & b3 in N & not b2 in M & not a3 in N & o <> a1 & o <> a2 & o <> a3 & o <> b1 & o <> b2 & o <> b3 & a3,b2 // a2,b1 & a3,b3 // a1,b1 holds
a1,b2 // a2,b3
let M, N be Subset of X; ( M is being_line & N is being_line & o in M & a1 in M & a2 in M & a3 in M & o in N & b1 in N & b2 in N & b3 in N & not b2 in M & not a3 in N & o <> a1 & o <> a2 & o <> a3 & o <> b1 & o <> b2 & o <> b3 & a3,b2 // a2,b1 & a3,b3 // a1,b1 implies a1,b2 // a2,b3 )
assume that
A3:
M is being_line
and
A4:
N is being_line
and
A5:
o in M
and
A6:
a1 in M
and
A7:
a2 in M
and
A8:
a3 in M
and
A9:
o in N
and
A10:
b1 in N
and
A11:
b2 in N
and
A12:
b3 in N
and
A13:
not b2 in M
and
A14:
not a3 in N
and
A15:
o <> a1
and
A16:
o <> a2
and
o <> a3
and
A17:
o <> b1
and
o <> b2
and
A18:
o <> b3
and
A19:
a3,b2 // a2,b1
and
A20:
a3,b3 // a1,b1
; a1,b2 // a2,b3
reconsider o9 = o, a19 = a1, a29 = a2, a39 = a3, b19 = b1, b29 = b2, b39 = b3 as Element of AffinStruct(# the carrier of X, the CONGR of X #) ;
reconsider M9 = M, N9 = N as Subset of AffinStruct(# the carrier of X, the CONGR of X #) ;
A21:
M9 is being_line
by A3, ANALMETR:43;
A22:
N9 is being_line
by A4, ANALMETR:43;
now ( not M _|_ N implies a1,b2 // a2,b3 )assume A23:
not
M _|_ N
;
a1,b2 // a2,b3A24:
now ( a1 <> a2 & a2 <> a3 & a1 <> a3 implies a1,b2 // a2,b3 )assume that A25:
a1 <> a2
and A26:
a2 <> a3
and A27:
a1 <> a3
;
a1,b2 // a2,b3A28:
(
b1 <> b2 &
b2 <> b3 &
b1 <> b3 )
proof
A29:
now not b1 = b3A30:
not
LIN o9,
b19,
a19
proof
o9,
a19 // o9,
a39
by A5, A6, A8, A21, AFF_1:39, AFF_1:41;
then A31:
LIN o9,
a19,
a39
by AFF_1:def 1;
assume
LIN o9,
b19,
a19
;
contradiction
then
a19 in N9
by A9, A10, A17, A22, AFF_1:25;
hence
contradiction
by A9, A14, A15, A22, A31, AFF_1:25;
verum
end; assume
b1 = b3
;
contradictionthen
b1,
a1 // b1,
a3
by A20, ANALMETR:59;
then A32:
b19,
a19 // b19,
a39
by ANALMETR:36;
o9,
a19 // o9,
a39
by A5, A6, A8, A21, AFF_1:39, AFF_1:41;
then
LIN o9,
a19,
a39
by AFF_1:def 1;
hence
contradiction
by A27, A30, A32, AFF_1:14;
verum end;
A33:
now not b2 = b3A34:
not
LIN o9,
b19,
a19
proof
o9,
a19 // o9,
a39
by A5, A6, A8, A21, AFF_1:39, AFF_1:41;
then A35:
LIN o9,
a19,
a39
by AFF_1:def 1;
assume
LIN o9,
b19,
a19
;
contradiction
then
a19 in N9
by A9, A10, A17, A22, AFF_1:25;
hence
contradiction
by A9, A14, A15, A22, A35, AFF_1:25;
verum
end; assume
b2 = b3
;
contradictionthen
a1,
b1 // a2,
b1
by A8, A13, A19, A20, ANALMETR:60;
then
b1,
a1 // b1,
a2
by ANALMETR:59;
then A36:
b19,
a19 // b19,
a29
by ANALMETR:36;
o9,
a19 // o9,
a29
by A5, A6, A7, A21, AFF_1:39, AFF_1:41;
then
LIN o9,
a19,
a29
by AFF_1:def 1;
hence
contradiction
by A25, A34, A36, AFF_1:14;
verum end;
A37:
now not b1 = b2A38:
not
LIN o9,
b29,
a29
assume
b1 = b2
;
contradictionthen
b2,
a2 // b2,
a3
by A19, ANALMETR:59;
then A39:
b29,
a29 // b29,
a39
by ANALMETR:36;
o9,
a29 // o9,
a39
by A5, A7, A8, A21, AFF_1:39, AFF_1:41;
then
LIN o9,
a29,
a39
by AFF_1:def 1;
hence
contradiction
by A26, A38, A39, AFF_1:14;
verum end;
assume
(
b1 = b2 or
b2 = b3 or
b1 = b3 )
;
contradiction
hence
contradiction
by A37, A33, A29;
verum
end; A40:
now ( not a3,b3 _|_ o,b2 implies a1,b2 // a2,b3 )A41:
not
LIN b3,
b1,
a3
o9,
b29 // o9,
b39
by A9, A11, A12, A22, AFF_1:39, AFF_1:41;
then
LIN o9,
b29,
b39
by AFF_1:def 1;
then A42:
LIN o,
b2,
b3
by ANALMETR:40;
A43:
not
LIN b2,
b1,
a3
o9,
a39 // o9,
a19
by A5, A6, A8, A21, AFF_1:39, AFF_1:41;
then
LIN o9,
a39,
a19
by AFF_1:def 1;
then A44:
LIN o,
a3,
a1
by ANALMETR:40;
consider x being
Element of
X such that A45:
o,
b2 _|_ o,
x
and A46:
o <> x
by ANALMETR:39;
A47:
o,
x _|_ N
by A4, A5, A9, A11, A13, A45, ANALMETR:55;
consider e19 being
Element of
AffinStruct(# the
carrier of
X, the
CONGR of
X #)
such that A48:
a39,
b39 // b29,
e19
and A49:
b29 <> e19
by DIRAF:40;
reconsider x9 =
x as
Element of
AffinStruct(# the
carrier of
X, the
CONGR of
X #) ;
LIN o9,
x9,
x9
by AFF_1:7;
then consider A9 being
Subset of
AffinStruct(# the
carrier of
X, the
CONGR of
X #)
such that A50:
A9 is
being_line
and A51:
o9 in A9
and A52:
x9 in A9
and
x9 in A9
by AFF_1:21;
reconsider A =
A9 as
Subset of
X ;
A53:
for
e1 being
Element of
X st
e1 in A holds
LIN o,
x,
e1
proof
let e1 be
Element of
X;
( e1 in A implies LIN o,x,e1 )
assume A54:
e1 in A
;
LIN o,x,e1
reconsider e19 =
e1 as
Element of
AffinStruct(# the
carrier of
X, the
CONGR of
X #) ;
o9,
x9 // o9,
e19
by A50, A51, A52, A54, AFF_1:39, AFF_1:41;
then
LIN o9,
x9,
e19
by AFF_1:def 1;
hence
LIN o,
x,
e1
by ANALMETR:40;
verum
end;
for
e1 being
Element of
X st
LIN o,
x,
e1 holds
e1 in A
proof
let e1 be
Element of
X;
( LIN o,x,e1 implies e1 in A )
assume A55:
LIN o,
x,
e1
;
e1 in A
reconsider e19 =
e1 as
Element of
AffinStruct(# the
carrier of
X, the
CONGR of
X #) ;
LIN o9,
x9,
e19
by A55, ANALMETR:40;
hence
e1 in A
by A46, A50, A51, A52, AFF_1:25;
verum
end; then
A = Line (
o,
x)
by A53, ANALMETR:def 11;
then A56:
A _|_ N
by A46, A47, ANALMETR:def 14;
A57:
not
b2 in A
proof
A58:
o9,
b29 // o9,
b29
by AFF_1:2;
assume
b2 in A
;
contradiction
then
A9 // N9
by A5, A9, A11, A13, A22, A50, A51, A58, AFF_1:38;
then
A // N
by ANALMETR:46;
hence
contradiction
by A56, ANALMETR:52;
verum
end; assume A59:
not
a3,
b3 _|_ o,
b2
;
a1,b2 // a2,b3
not
b29,
e19 // A9
proof
assume A60:
b29,
e19 // A9
;
contradiction
consider d19,
d29 being
Element of
AffinStruct(# the
carrier of
X, the
CONGR of
X #)
such that A61:
d19 <> d29
and A62:
A9 = Line (
d19,
d29)
by A50, AFF_1:def 3;
A63:
d29 in A9
by A62, AFF_1:15;
reconsider d1 =
d19,
d2 =
d29 as
Element of
X ;
d19,
d29 // d19,
d29
by AFF_1:2;
then
d19,
d29 // A9
by A61, A62, AFF_1:def 4;
then
b29,
e19 // d19,
d29
by A50, A60, AFF_1:31;
then
a39,
b39 // d19,
d29
by A48, A49, AFF_1:5;
then A64:
a3,
b3 // d1,
d2
by ANALMETR:36;
d19 in A9
by A62, AFF_1:15;
then
d1,
d2 _|_ o,
b2
by A9, A11, A56, A63, ANALMETR:56;
hence
contradiction
by A59, A61, A64, ANALMETR:62;
verum
end; then consider c39 being
Element of
AffinStruct(# the
carrier of
X, the
CONGR of
X #)
such that A65:
c39 in A9
and A66:
LIN b29,
e19,
c39
by A50, AFF_1:59;
b29,
e19 // b29,
c39
by A66, AFF_1:def 1;
then A67:
a39,
b39 // b29,
c39
by A48, A49, AFF_1:5;
consider e19 being
Element of
AffinStruct(# the
carrier of
X, the
CONGR of
X #)
such that A68:
c39,
a39 // a19,
e19
and A69:
a19 <> e19
by DIRAF:40;
not
a19,
e19 // A9
proof
A70:
c39 <> o9
proof
assume
c39 = o9
;
contradiction
then A71:
a3,
b3 // b2,
o
by A67, ANALMETR:36;
b29,
o9 // b29,
b39
by A9, A11, A12, A22, AFF_1:39, AFF_1:41;
then
b2,
o // b2,
b3
by ANALMETR:36;
then
a3,
b3 // b2,
b3
by A5, A13, A71, ANALMETR:60;
then
b3,
b2 // b3,
a3
by ANALMETR:59;
then
LIN b3,
b2,
a3
by ANALMETR:def 10;
then
LIN b39,
b29,
a39
by ANALMETR:40;
hence
contradiction
by A11, A12, A14, A22, A28, AFF_1:25;
verum
end;
assume A72:
a19,
e19 // A9
;
contradiction
A73:
o9,
a39 // o9,
a39
by AFF_1:2;
o9,
c39 // A9
by A50, A51, A65, AFF_1:40, AFF_1:41;
then
a19,
e19 // o9,
c39
by A50, A72, AFF_1:31;
then
c39,
a39 // o9,
c39
by A68, A69, AFF_1:5;
then
c39,
o9 // c39,
a39
by AFF_1:4;
then
LIN c39,
o9,
a39
by AFF_1:def 1;
then
a39 in A9
by A50, A51, A65, A70, AFF_1:25;
then
A9 // M9
by A5, A8, A9, A14, A21, A50, A51, A73, AFF_1:38;
then
A // M
by ANALMETR:46;
hence
contradiction
by A23, A56, ANALMETR:52;
verum
end; then consider c19 being
Element of
AffinStruct(# the
carrier of
X, the
CONGR of
X #)
such that A74:
c19 in A9
and A75:
LIN a19,
e19,
c19
by A50, AFF_1:59;
reconsider c1 =
c19 as
Element of
X ;
reconsider c3 =
c39 as
Element of
X ;
a19,
e19 // a19,
c19
by A75, AFF_1:def 1;
then A76:
c39,
a39 // a19,
c19
by A68, A69, AFF_1:5;
then A77:
c3,
a3 // a1,
c1
by ANALMETR:36;
consider e19 being
Element of
AffinStruct(# the
carrier of
X, the
CONGR of
X #)
such that A78:
c39,
a39 // a29,
e19
and A79:
a29 <> e19
by DIRAF:40;
not
a29,
e19 // A9
proof
A80:
c39 <> o9
proof
assume
c39 = o9
;
contradiction
then A81:
a3,
b3 // b2,
o
by A67, ANALMETR:36;
b29,
o9 // b29,
b39
by A9, A11, A12, A22, AFF_1:39, AFF_1:41;
then
b2,
o // b2,
b3
by ANALMETR:36;
then
a3,
b3 // b2,
b3
by A5, A13, A81, ANALMETR:60;
then
b3,
b2 // b3,
a3
by ANALMETR:59;
then
LIN b3,
b2,
a3
by ANALMETR:def 10;
then
LIN b39,
b29,
a39
by ANALMETR:40;
hence
contradiction
by A11, A12, A14, A22, A28, AFF_1:25;
verum
end;
assume A82:
a29,
e19 // A9
;
contradiction
A83:
o9,
a39 // o9,
a39
by AFF_1:2;
o9,
c39 // A9
by A50, A51, A65, AFF_1:40, AFF_1:41;
then
a29,
e19 // o9,
c39
by A50, A82, AFF_1:31;
then
c39,
a39 // o9,
c39
by A78, A79, AFF_1:5;
then
c39,
o9 // c39,
a39
by AFF_1:4;
then
LIN c39,
o9,
a39
by AFF_1:def 1;
then
a39 in A9
by A50, A51, A65, A80, AFF_1:25;
then
A9 // M9
by A5, A8, A9, A14, A21, A50, A51, A83, AFF_1:38;
then
A // M
by ANALMETR:46;
hence
contradiction
by A23, A56, ANALMETR:52;
verum
end; then consider c29 being
Element of
AffinStruct(# the
carrier of
X, the
CONGR of
X #)
such that A84:
c29 in A9
and A85:
LIN a29,
e19,
c29
by A50, AFF_1:59;
reconsider c2 =
c29 as
Element of
X ;
a29,
e19 // a29,
c29
by A85, AFF_1:def 1;
then A86:
c39,
a39 // a29,
c29
by A78, A79, AFF_1:5;
then A87:
c3,
a3 // a2,
c2
by ANALMETR:36;
A88:
(
o <> c3 &
o <> c2 &
o <> c1 )
proof
A89:
now not o = c3assume A90:
o = c3
;
contradiction
b29,
o9 // b39,
b29
by A9, A11, A12, A22, AFF_1:39, AFF_1:41;
then
a39,
b39 // b39,
b29
by A5, A13, A67, A90, AFF_1:5;
then
b39,
b29 // b39,
a39
by AFF_1:4;
then
LIN b39,
b29,
a39
by AFF_1:def 1;
hence
contradiction
by A11, A12, A14, A22, A28, AFF_1:25;
verum end;
A91:
now ( not o = c2 & not o = c1 )
a19,
o9 // a19,
a39
by A5, A6, A8, A21, AFF_1:39, AFF_1:41;
then A92:
a1,
o // a1,
a3
by ANALMETR:36;
assume
(
o = c2 or
o = c1 )
;
contradictionthen A93:
(
c3,
a3 // a1,
o or
c3,
a3 // a2,
o )
by A76, A86, ANALMETR:36;
a29,
o9 // a19,
a39
by A5, A6, A7, A8, A21, AFF_1:39, AFF_1:41;
then
a2,
o // a1,
a3
by ANALMETR:36;
then
c3,
a3 // a1,
a3
by A15, A16, A93, A92, ANALMETR:60;
then
a3,
a1 // a3,
c3
by ANALMETR:59;
then
LIN a3,
a1,
c3
by ANALMETR:def 10;
then
LIN a39,
a19,
c39
by ANALMETR:40;
then A94:
c39 in M9
by A6, A8, A21, A27, AFF_1:25;
o9,
c39 // o9,
c39
by AFF_1:2;
then
A9 // M9
by A5, A21, A50, A51, A65, A89, A94, AFF_1:38;
then
A // M
by ANALMETR:46;
hence
contradiction
by A23, A56, ANALMETR:52;
verum end;
assume
(
o = c3 or
o = c2 or
o = c1 )
;
contradiction
hence
contradiction
by A89, A91;
verum
end; A95:
not
c3 in N
proof
A96:
o9,
c39 // o9,
c39
by AFF_1:2;
assume
c3 in N
;
contradiction
then
A9 // N9
by A9, A22, A50, A51, A65, A88, A96, AFF_1:38;
then
A // N
by ANALMETR:46;
hence
contradiction
by A56, ANALMETR:52;
verum
end; A97:
not
LIN a3,
a2,
c3
proof
assume
LIN a3,
a2,
c3
;
contradiction
then
LIN a39,
a29,
c39
by ANALMETR:40;
then A98:
c39 in M9
by A7, A8, A21, A26, AFF_1:25;
o9,
c39 // o9,
c39
by AFF_1:2;
then
A9 // M9
by A5, A21, A50, A51, A65, A88, A98, AFF_1:38;
then
A // M
by ANALMETR:46;
hence
contradiction
by A23, A56, ANALMETR:52;
verum
end; A99:
not
LIN a3,
a1,
c3
proof
assume
LIN a3,
a1,
c3
;
contradiction
then
LIN a39,
a19,
c39
by ANALMETR:40;
then A100:
c39 in M9
by A6, A8, A21, A27, AFF_1:25;
o9,
c39 // o9,
c39
by AFF_1:2;
then
A9 // M9
by A5, A21, A50, A51, A65, A88, A100, AFF_1:38;
then
A // M
by ANALMETR:46;
hence
contradiction
by A23, A56, ANALMETR:52;
verum
end; A101:
not
LIN a1,
a2,
c1
proof
assume
LIN a1,
a2,
c1
;
contradiction
then
LIN a19,
a29,
c19
by ANALMETR:40;
then A102:
c19 in M9
by A6, A7, A21, A25, AFF_1:25;
o9,
c19 // o9,
c19
by AFF_1:2;
then
M9 // A9
by A5, A21, A50, A51, A74, A88, A102, AFF_1:38;
then
M // A
by ANALMETR:46;
hence
contradiction
by A23, A56, ANALMETR:52;
verum
end;
o9,
a19 // o9,
a29
by A5, A6, A7, A21, AFF_1:39, AFF_1:41;
then
LIN o9,
a19,
a29
by AFF_1:def 1;
then A103:
LIN o,
a1,
a2
by ANALMETR:40;
o9,
b29 // o9,
b19
by A9, A10, A11, A22, AFF_1:39, AFF_1:41;
then
LIN o9,
b29,
b19
by AFF_1:def 1;
then A104:
LIN o,
b2,
b1
by ANALMETR:40;
o9,
c19 // o9,
c29
by A50, A51, A74, A84, AFF_1:39, AFF_1:41;
then
LIN o9,
c19,
c29
by AFF_1:def 1;
then A105:
LIN o,
c1,
c2
by ANALMETR:40;
o9,
c39 // o9,
c29
by A50, A51, A65, A84, AFF_1:39, AFF_1:41;
then
LIN o9,
c39,
c29
by AFF_1:def 1;
then A106:
LIN o,
c3,
c2
by ANALMETR:40;
o9,
c39 // o9,
c19
by A50, A51, A65, A74, AFF_1:39, AFF_1:41;
then
LIN o9,
c39,
c19
by AFF_1:def 1;
then A107:
LIN o,
c3,
c1
by ANALMETR:40;
c3 <> a3
proof
A108:
o9,
a39 // o9,
a39
by AFF_1:2;
assume
c3 = a3
;
contradiction
then
A9 // M9
by A5, A8, A9, A14, A21, A50, A51, A65, A108, AFF_1:38;
then
A // M
by ANALMETR:46;
hence
contradiction
by A23, A56, ANALMETR:52;
verum
end; then
a1,
c1 // a2,
c2
by A77, A87, ANALMETR:60;
then A109:
c1,
a1 // c2,
a2
by ANALMETR:59;
A110:
not
LIN c1,
c2,
b2
proof
A111:
c19 <> c29
proof
A112:
c3 <> a3
proof
A113:
o9,
c39 // o9,
c39
by AFF_1:2;
assume
c3 = a3
;
contradiction
then
A9 // M9
by A5, A8, A9, A14, A21, A50, A51, A65, A113, AFF_1:38;
then
A // M
by ANALMETR:46;
hence
contradiction
by A23, A56, ANALMETR:52;
verum
end;
assume
c19 = c29
;
contradiction
then
a1,
c1 // a2,
c1
by A77, A87, A112, ANALMETR:60;
then
c1,
a2 // c1,
a1
by ANALMETR:59;
then
LIN c1,
a2,
a1
by ANALMETR:def 10;
then
LIN c19,
a29,
a19
by ANALMETR:40;
then
LIN a19,
a29,
c19
by AFF_1:6;
then A114:
c19 in M9
by A6, A7, A21, A25, AFF_1:25;
o9,
c19 // o9,
c19
by AFF_1:2;
then
A9 // M9
by A5, A21, A50, A51, A74, A88, A114, AFF_1:38;
then
A // M
by ANALMETR:46;
hence
contradiction
by A23, A56, ANALMETR:52;
verum
end;
assume
LIN c1,
c2,
b2
;
contradiction
then
LIN c19,
c29,
b29
by ANALMETR:40;
then
b29 in A9
by A50, A74, A84, A111, AFF_1:25;
then
A9 = N9
by A5, A9, A11, A13, A22, A50, A51, AFF_1:18;
then
A9 // N9
by A22, AFF_1:41;
then
A // N
by ANALMETR:46;
hence
contradiction
by A56, ANALMETR:52;
verum
end;
o9,
a39 // o9,
a29
by A5, A7, A8, A21, AFF_1:39, AFF_1:41;
then
LIN o9,
a39,
a29
by AFF_1:def 1;
then A115:
LIN o,
a3,
a2
by ANALMETR:40;
o9,
b39 // o9,
b19
by A9, A10, A12, A22, AFF_1:39, AFF_1:41;
then
LIN o9,
b39,
b19
by AFF_1:def 1;
then A116:
LIN o,
b3,
b1
by ANALMETR:40;
a3,
c3 // a1,
c1
by A77, ANALMETR:59;
then
b3,
c3 // b1,
c1
by A2, A9, A14, A15, A17, A18, A20, A88, A99, A41, A44, A116, A107, CONAFFM:def 1;
then A117:
c3,
b3 // c1,
b1
by ANALMETR:59;
a3,
c3 // a2,
c2
by A87, ANALMETR:59;
then
b2,
c3 // b1,
c2
by A2, A5, A9, A13, A14, A16, A17, A19, A88, A115, A104, A106, A43, A97, CONAFFM:def 1;
then
c3,
b2 // c2,
b1
by ANALMETR:59;
then
c1,
b2 // c2,
b3
by A1, A9, A10, A11, A12, A17, A18, A51, A56, A65, A74, A84, A88, A117, A57, A95;
hence
a1,
b2 // a2,
b3
by A2, A5, A13, A15, A16, A18, A88, A103, A42, A105, A101, A110, A109, CONAFFM:def 1;
verum end; now ( a3,b3 _|_ o,b2 implies a1,b2 // a2,b3 )
o9,
a19 // o9,
a29
by A5, A6, A7, A21, AFF_1:39, AFF_1:41;
then
LIN o9,
a19,
a29
by AFF_1:def 1;
then A118:
LIN o,
a1,
a2
by ANALMETR:40;
o9,
b29 // o9,
b19
by A9, A10, A11, A22, AFF_1:39, AFF_1:41;
then
LIN o9,
b29,
b19
by AFF_1:def 1;
then A119:
LIN o,
b2,
b1
by ANALMETR:40;
o9,
b29 // o9,
b39
by A9, A11, A12, A22, AFF_1:39, AFF_1:41;
then
LIN o9,
b29,
b39
by AFF_1:def 1;
then A120:
LIN o,
b2,
b3
by ANALMETR:40;
A121:
( not
LIN b3,
b1,
a3 & not
LIN b2,
b1,
a3 )
proof
assume
(
LIN b3,
b1,
a3 or
LIN b2,
b1,
a3 )
;
contradiction
then
(
LIN b39,
b19,
a39 or
LIN b29,
b19,
a39 )
by ANALMETR:40;
hence
contradiction
by A10, A11, A12, A14, A22, A28, AFF_1:25;
verum
end;
o9,
a39 // o9,
a29
by A5, A7, A8, A21, AFF_1:39, AFF_1:41;
then
LIN o9,
a39,
a29
by AFF_1:def 1;
then A122:
LIN o,
a3,
a2
by ANALMETR:40;
o9,
b39 // o9,
b19
by A9, A10, A12, A22, AFF_1:39, AFF_1:41;
then
LIN o9,
b39,
b19
by AFF_1:def 1;
then A123:
LIN o,
b3,
b1
by ANALMETR:40;
o9,
a39 // o9,
a19
by A5, A6, A8, A21, AFF_1:39, AFF_1:41;
then
LIN o9,
a39,
a19
by AFF_1:def 1;
then A124:
LIN o,
a3,
a1
by ANALMETR:40;
consider x being
Element of
X such that A125:
o,
b2 _|_ o,
x
and A126:
o <> x
by ANALMETR:39;
A127:
o,
x _|_ N
by A4, A5, A9, A11, A13, A125, ANALMETR:55;
consider e19 being
Element of
AffinStruct(# the
carrier of
X, the
CONGR of
X #)
such that A128:
a39,
b29 // b39,
e19
and A129:
b39 <> e19
by DIRAF:40;
reconsider x9 =
x as
Element of
AffinStruct(# the
carrier of
X, the
CONGR of
X #) ;
LIN o9,
x9,
x9
by AFF_1:7;
then consider A9 being
Subset of
AffinStruct(# the
carrier of
X, the
CONGR of
X #)
such that A130:
A9 is
being_line
and A131:
o9 in A9
and A132:
x9 in A9
and
x9 in A9
by AFF_1:21;
reconsider A =
A9 as
Subset of
X ;
A133:
for
e1 being
Element of
X st
e1 in A holds
LIN o,
x,
e1
proof
let e1 be
Element of
X;
( e1 in A implies LIN o,x,e1 )
assume A134:
e1 in A
;
LIN o,x,e1
reconsider e19 =
e1 as
Element of
AffinStruct(# the
carrier of
X, the
CONGR of
X #) ;
o9,
x9 // o9,
e19
by A130, A131, A132, A134, AFF_1:39, AFF_1:41;
then
LIN o9,
x9,
e19
by AFF_1:def 1;
hence
LIN o,
x,
e1
by ANALMETR:40;
verum
end;
for
e1 being
Element of
X st
LIN o,
x,
e1 holds
e1 in A
proof
let e1 be
Element of
X;
( LIN o,x,e1 implies e1 in A )
assume A135:
LIN o,
x,
e1
;
e1 in A
reconsider e19 =
e1 as
Element of
AffinStruct(# the
carrier of
X, the
CONGR of
X #) ;
LIN o9,
x9,
e19
by A135, ANALMETR:40;
hence
e1 in A
by A126, A130, A131, A132, AFF_1:25;
verum
end; then
A = Line (
o,
x)
by A133, ANALMETR:def 11;
then A136:
A _|_ N
by A126, A127, ANALMETR:def 14;
assume A137:
a3,
b3 _|_ o,
b2
;
a1,b2 // a2,b3
not
b39,
e19 // A9
proof
assume A138:
b39,
e19 // A9
;
contradiction
consider d19,
d29 being
Element of
AffinStruct(# the
carrier of
X, the
CONGR of
X #)
such that A139:
d19 <> d29
and A140:
A9 = Line (
d19,
d29)
by A130, AFF_1:def 3;
A141:
d29 in A9
by A140, AFF_1:15;
reconsider d1 =
d19,
d2 =
d29 as
Element of
X ;
d19,
d29 // d19,
d29
by AFF_1:2;
then
d19,
d29 // A9
by A139, A140, AFF_1:def 4;
then
b39,
e19 // d19,
d29
by A130, A138, AFF_1:31;
then
a39,
b29 // d19,
d29
by A128, A129, AFF_1:5;
then A142:
a3,
b2 // d1,
d2
by ANALMETR:36;
d19 in A9
by A140, AFF_1:15;
then
d1,
d2 _|_ o,
b2
by A9, A11, A136, A141, ANALMETR:56;
then
a3,
b2 _|_ o,
b2
by A139, A142, ANALMETR:62;
then
a3,
b2 // a3,
b3
by A5, A13, A137, ANALMETR:63;
then
LIN a3,
b2,
b3
by ANALMETR:def 10;
then
LIN a39,
b29,
b39
by ANALMETR:40;
then
LIN b29,
b39,
a39
by AFF_1:6;
hence
contradiction
by A11, A12, A14, A22, A28, AFF_1:25;
verum
end; then consider c39 being
Element of
AffinStruct(# the
carrier of
X, the
CONGR of
X #)
such that A143:
c39 in A9
and A144:
LIN b39,
e19,
c39
by A130, AFF_1:59;
A145:
b39,
e19 // b39,
c39
by A144, AFF_1:def 1;
consider e19 being
Element of
AffinStruct(# the
carrier of
X, the
CONGR of
X #)
such that A146:
c39,
a39 // a29,
e19
and A147:
a29 <> e19
by DIRAF:40;
not
a29,
e19 // A9
proof
A148:
c39 <> o9
proof
assume
c39 = o9
;
contradiction
then A149:
a39,
b29 // b39,
o9
by A128, A129, A145, AFF_1:5;
b39,
o9 // b39,
b29
by A9, A11, A12, A22, AFF_1:39, AFF_1:41;
then
a39,
b29 // b39,
b29
by A18, A149, AFF_1:5;
then
b29,
b39 // b29,
a39
by AFF_1:4;
then
LIN b29,
b39,
a39
by AFF_1:def 1;
hence
contradiction
by A11, A12, A14, A22, A28, AFF_1:25;
verum
end;
assume A150:
a29,
e19 // A9
;
contradiction
A151:
o9,
a39 // o9,
a39
by AFF_1:2;
o9,
c39 // A9
by A130, A131, A143, AFF_1:40, AFF_1:41;
then
a29,
e19 // o9,
c39
by A130, A150, AFF_1:31;
then
c39,
a39 // o9,
c39
by A146, A147, AFF_1:5;
then
c39,
o9 // c39,
a39
by AFF_1:4;
then
LIN c39,
o9,
a39
by AFF_1:def 1;
then
a39 in A9
by A130, A131, A143, A148, AFF_1:25;
then
A9 // M9
by A5, A8, A9, A14, A21, A130, A131, A151, AFF_1:38;
then
A // M
by ANALMETR:46;
hence
contradiction
by A23, A136, ANALMETR:52;
verum
end; then consider c29 being
Element of
AffinStruct(# the
carrier of
X, the
CONGR of
X #)
such that A152:
c29 in A9
and A153:
LIN a29,
e19,
c29
by A130, AFF_1:59;
reconsider c3 =
c39 as
Element of
X ;
reconsider c2 =
c29 as
Element of
X ;
a29,
e19 // a29,
c29
by A153, AFF_1:def 1;
then
c39,
a39 // a29,
c29
by A146, A147, AFF_1:5;
then A154:
c3,
a3 // a2,
c2
by ANALMETR:36;
then A155:
a3,
c3 // a2,
c2
by ANALMETR:59;
consider e19 being
Element of
AffinStruct(# the
carrier of
X, the
CONGR of
X #)
such that A156:
c39,
a39 // a19,
e19
and A157:
a19 <> e19
by DIRAF:40;
not
a19,
e19 // A9
proof
A158:
c39 <> o9
proof
assume
c39 = o9
;
contradiction
then A159:
a39,
b29 // b39,
o9
by A128, A129, A145, AFF_1:5;
b39,
o9 // b39,
b29
by A9, A11, A12, A22, AFF_1:39, AFF_1:41;
then
a39,
b29 // b39,
b29
by A18, A159, AFF_1:5;
then
b29,
b39 // b29,
a39
by AFF_1:4;
then
LIN b29,
b39,
a39
by AFF_1:def 1;
hence
contradiction
by A11, A12, A14, A22, A28, AFF_1:25;
verum
end;
assume A160:
a19,
e19 // A9
;
contradiction
A161:
o9,
a39 // o9,
a39
by AFF_1:2;
o9,
c39 // A9
by A130, A131, A143, AFF_1:40, AFF_1:41;
then
a19,
e19 // o9,
c39
by A130, A160, AFF_1:31;
then
c39,
a39 // o9,
c39
by A156, A157, AFF_1:5;
then
c39,
o9 // c39,
a39
by AFF_1:4;
then
LIN c39,
o9,
a39
by AFF_1:def 1;
then
a39 in A9
by A130, A131, A143, A158, AFF_1:25;
then
A9 // M9
by A5, A8, A9, A14, A21, A130, A131, A161, AFF_1:38;
then
A // M
by ANALMETR:46;
hence
contradiction
by A23, A136, ANALMETR:52;
verum
end; then consider c19 being
Element of
AffinStruct(# the
carrier of
X, the
CONGR of
X #)
such that A162:
c19 in A9
and A163:
LIN a19,
e19,
c19
by A130, AFF_1:59;
reconsider c1 =
c19 as
Element of
X ;
a19,
e19 // a19,
c19
by A163, AFF_1:def 1;
then
c39,
a39 // a19,
c19
by A156, A157, AFF_1:5;
then A164:
c3,
a3 // a1,
c1
by ANALMETR:36;
then A165:
a3,
c3 // a1,
c1
by ANALMETR:59;
A166:
a39,
b29 // b39,
c39
by A128, A129, A145, AFF_1:5;
A167:
(
o <> c3 &
o <> c2 &
o <> c1 )
proof
A168:
now not o = c3assume
o = c3
;
contradictionthen A169:
a3,
b2 // b3,
o
by A166, ANALMETR:36;
b39,
o9 // b29,
b39
by A9, A11, A12, A22, AFF_1:39, AFF_1:41;
then
b3,
o // b2,
b3
by ANALMETR:36;
then
a3,
b2 // b2,
b3
by A18, A169, ANALMETR:60;
then
b2,
b3 // b2,
a3
by ANALMETR:59;
then
LIN b2,
b3,
a3
by ANALMETR:def 10;
then
LIN b29,
b39,
a39
by ANALMETR:40;
hence
contradiction
by A11, A12, A14, A22, A28, AFF_1:25;
verum end;
A170:
now ( not o = c2 & not o = c1 )
a29,
o9 // a29,
a39
by A5, A7, A8, A21, AFF_1:39, AFF_1:41;
then A171:
a2,
o // a2,
a3
by ANALMETR:36;
assume
(
o = c2 or
o = c1 )
;
contradictionthen A172:
(
a3,
c3 // a2,
o or
a3,
c3 // a1,
o )
by A154, A164, ANALMETR:59;
a19,
o9 // a29,
a39
by A5, A6, A7, A8, A21, AFF_1:39, AFF_1:41;
then
a1,
o // a2,
a3
by ANALMETR:36;
then
a3,
c3 // a2,
a3
by A15, A16, A172, A171, ANALMETR:60;
then
a3,
a2 // a3,
c3
by ANALMETR:59;
then
LIN a3,
a2,
c3
by ANALMETR:def 10;
then
LIN a39,
a29,
c39
by ANALMETR:40;
then A173:
c39 in M9
by A7, A8, A21, A26, AFF_1:25;
o9,
c39 // o9,
c39
by AFF_1:2;
then
A9 // M9
by A5, A21, A130, A131, A143, A168, A173, AFF_1:38;
then
A // M
by ANALMETR:46;
hence
contradiction
by A23, A136, ANALMETR:52;
verum end;
assume
(
o = c3 or
o = c2 or
o = c1 )
;
contradiction
hence
contradiction
by A168, A170;
verum
end; A174:
not
c3 in N
proof
A175:
o9,
c39 // o9,
c39
by AFF_1:2;
assume
c3 in N
;
contradiction
then
A9 // N9
by A9, A22, A130, A131, A143, A167, A175, AFF_1:38;
then
A // N
by ANALMETR:46;
hence
contradiction
by A136, ANALMETR:52;
verum
end; A176:
not
LIN a1,
a2,
c1
proof
assume
LIN a1,
a2,
c1
;
contradiction
then
LIN a19,
a29,
c19
by ANALMETR:40;
then A177:
c19 in M9
by A6, A7, A21, A25, AFF_1:25;
o9,
c19 // o9,
c19
by AFF_1:2;
then
A9 // M9
by A5, A21, A130, A131, A162, A167, A177, AFF_1:38;
then
A // M
by ANALMETR:46;
hence
contradiction
by A23, A136, ANALMETR:52;
verum
end; A178:
( not
LIN a3,
a1,
c3 & not
LIN a3,
a2,
c3 )
proof
assume
(
LIN a3,
a1,
c3 or
LIN a3,
a2,
c3 )
;
contradiction
then
(
LIN a39,
a19,
c39 or
LIN a39,
a29,
c39 )
by ANALMETR:40;
then A179:
(
c39 in M9 or
c39 in M9 )
by A6, A7, A8, A21, A26, A27, AFF_1:25;
o9,
c39 // o9,
c39
by AFF_1:2;
then
A9 // M9
by A5, A21, A130, A131, A143, A167, A179, AFF_1:38;
then
A // M
by ANALMETR:46;
hence
contradiction
by A23, A136, ANALMETR:52;
verum
end; A180:
not
b2 in A
proof
A181:
o9,
b29 // o9,
b29
by AFF_1:2;
assume
b2 in A
;
contradiction
then
A9 // N9
by A5, A9, A11, A13, A22, A130, A131, A181, AFF_1:38;
then
A // N
by ANALMETR:46;
hence
contradiction
by A136, ANALMETR:52;
verum
end; A182:
not
LIN c1,
c2,
b2
proof
A183:
c19 <> c29
proof
A184:
a3 <> c3
proof
A185:
o9,
c39 // o9,
c39
by AFF_1:2;
assume
a3 = c3
;
contradiction
then
A9 // M9
by A5, A8, A9, A14, A21, A130, A131, A143, A185, AFF_1:38;
then
A // M
by ANALMETR:46;
hence
contradiction
by A23, A136, ANALMETR:52;
verum
end;
assume
c19 = c29
;
contradiction
then
a2,
c1 // a1,
c1
by A155, A165, A184, ANALMETR:60;
then
c1,
a1 // c1,
a2
by ANALMETR:59;
then
LIN c1,
a1,
a2
by ANALMETR:def 10;
then
LIN c19,
a19,
a29
by ANALMETR:40;
then
LIN a19,
a29,
c19
by AFF_1:6;
then A186:
c19 in M9
by A6, A7, A21, A25, AFF_1:25;
o9,
c19 // o9,
c19
by AFF_1:2;
then
A9 // M9
by A5, A21, A130, A131, A162, A167, A186, AFF_1:38;
then
A // M
by ANALMETR:46;
hence
contradiction
by A23, A136, ANALMETR:52;
verum
end;
assume
LIN c1,
c2,
b2
;
contradiction
then
LIN c19,
c29,
b29
by ANALMETR:40;
hence
contradiction
by A130, A152, A162, A180, A183, AFF_1:25;
verum
end;
o9,
c19 // o9,
c29
by A130, A131, A152, A162, AFF_1:39, AFF_1:41;
then
LIN o9,
c19,
c29
by AFF_1:def 1;
then A187:
LIN o,
c1,
c2
by ANALMETR:40;
a3 <> c3
proof
A188:
o9,
a39 // o9,
a39
by AFF_1:2;
assume
a3 = c3
;
contradiction
then
A9 // M9
by A5, A8, A9, A14, A21, A130, A131, A143, A188, AFF_1:38;
then
A // M
by ANALMETR:46;
hence
contradiction
by A23, A136, ANALMETR:52;
verum
end; then
a2,
c2 // a1,
c1
by A155, A165, ANALMETR:60;
then A189:
c1,
a1 // c2,
a2
by ANALMETR:59;
o9,
c39 // o9,
c19
by A130, A131, A143, A162, AFF_1:39, AFF_1:41;
then
LIN o9,
c39,
c19
by AFF_1:def 1;
then
LIN o,
c3,
c1
by ANALMETR:40;
then
b3,
c3 // b1,
c1
by A2, A9, A14, A15, A17, A18, A20, A165, A167, A121, A178, A124, A123, CONAFFM:def 1;
then A190:
c3,
b3 // c1,
b1
by ANALMETR:59;
o9,
c39 // o9,
c29
by A130, A131, A143, A152, AFF_1:39, AFF_1:41;
then
LIN o9,
c39,
c29
by AFF_1:def 1;
then
LIN o,
c3,
c2
by ANALMETR:40;
then
b2,
c3 // b1,
c2
by A2, A5, A9, A13, A14, A16, A17, A19, A155, A167, A121, A178, A122, A119, CONAFFM:def 1;
then
c3,
b2 // c2,
b1
by ANALMETR:59;
then
c1,
b2 // c2,
b3
by A1, A9, A10, A11, A12, A17, A18, A131, A136, A143, A152, A162, A167, A190, A180, A174;
hence
a1,
b2 // a2,
b3
by A2, A5, A13, A15, A16, A18, A167, A118, A120, A187, A176, A182, A189, CONAFFM:def 1;
verum end; hence
a1,
b2 // a2,
b3
by A40;
verum end; A191:
now ( a1 = a3 implies a1,b2 // a2,b3 )A192:
not
LIN o9,
a39,
b39
o9,
b39 // o9,
b19
by A9, A10, A12, A22, AFF_1:39, AFF_1:41;
then A193:
LIN o9,
b39,
b19
by AFF_1:def 1;
assume A194:
a1 = a3
;
a1,b2 // a2,b3then
a39,
b39 // a39,
b19
by A20, ANALMETR:36;
hence
a1,
b2 // a2,
b3
by A19, A194, A192, A193, AFF_1:14;
verum end; A195:
now ( a1 = a2 implies a1,b2 // a2,b3 )
o9,
b29 // o9,
b39
by A9, A11, A12, A22, AFF_1:39, AFF_1:41;
then A196:
LIN o9,
b29,
b39
by AFF_1:def 1;
assume A197:
a1 = a2
;
a1,b2 // a2,b3
a1 <> b1
proof
o9,
a19 // o9,
a39
by A5, A6, A8, A21, AFF_1:39, AFF_1:41;
then A198:
LIN o9,
a19,
a39
by AFF_1:def 1;
assume
a1 = b1
;
contradiction
hence
contradiction
by A9, A10, A14, A15, A22, A198, AFF_1:25;
verum
end; then
a3,
b2 // a3,
b3
by A19, A20, A197, ANALMETR:60;
then
a39,
b29 // a39,
b39
by ANALMETR:36;
then
b29 = b39
by A5, A8, A9, A13, A14, A21, A196, AFF_1:14, AFF_1:25;
then
a19,
b29 // a29,
b39
by A197, AFF_1:2;
hence
a1,
b2 // a2,
b3
by ANALMETR:36;
verum end; now ( a2 = a3 implies a1,b2 // a2,b3 )
o9,
b29 // o9,
b19
by A9, A10, A11, A22, AFF_1:39, AFF_1:41;
then A199:
LIN o9,
b29,
b19
by AFF_1:def 1;
assume A200:
a2 = a3
;
a1,b2 // a2,b3then
a39,
b29 // a39,
b19
by A19, ANALMETR:36;
then
b29 = b19
by A5, A8, A9, A13, A14, A21, A199, AFF_1:14, AFF_1:25;
hence
a1,
b2 // a2,
b3
by A20, A200, ANALMETR:59;
verum end; hence
a1,
b2 // a2,
b3
by A195, A191, A24;
verum end;
hence
a1,b2 // a2,b3
by A1, A5, A6, A7, A8, A9, A10, A11, A12, A13, A14, A15, A16, A17, A18, A19, A20; verum