let X be OrtAfPl; ( X is satisfying_LIN implies X is satisfying_3H )
assume A1:
X is satisfying_LIN
; X is satisfying_3H
let a be Element of X; CONAFFM:def 3 for b, c being Element of X st not LIN a,b,c holds
ex d being Element of X st
( d,a _|_ b,c & d,b _|_ a,c & d,c _|_ a,b )
let b, c be Element of X; ( not LIN a,b,c implies ex d being Element of X st
( d,a _|_ b,c & d,b _|_ a,c & d,c _|_ a,b ) )
assume A2:
not LIN a,b,c
; ex d being Element of X st
( d,a _|_ b,c & d,b _|_ a,c & d,c _|_ a,b )
consider e1 being Element of X such that
A3:
b,c _|_ a,e1
and
A4:
a <> e1
by ANALMETR:def 9;
consider e2 being Element of X such that
A5:
a,c _|_ b,e2
and
A6:
b <> e2
by ANALMETR:def 9;
reconsider a9 = a, b9 = b, c9 = c, e19 = e1, e29 = e2 as Element of AffinStruct(# the U1 of X, the CONGR of X #) ;
not a9,e19 // b9,e29
proof
assume
a9,
e19 // b9,
e29
;
contradiction
then
a,
e1 // b,
e2
by ANALMETR:36;
then
b,
e2 _|_ b,
c
by A3, A4, ANALMETR:62;
then
a,
c // b,
c
by A5, A6, ANALMETR:63;
then
a9,
c9 // b9,
c9
by ANALMETR:36;
then
c9,
a9 // c9,
b9
by AFF_1:4;
then
LIN c9,
a9,
b9
by AFF_1:def 1;
then
LIN a9,
b9,
c9
by AFF_1:6;
hence
contradiction
by A2, ANALMETR:40;
verum
end;
then consider d9 being Element of AffinStruct(# the U1 of X, the CONGR of X #) such that
A7:
LIN a9,e19,d9
and
A8:
LIN b9,e29,d9
by AFF_1:60;
reconsider d = d9 as Element of X ;
take
d
; ( d,a _|_ b,c & d,b _|_ a,c & d,c _|_ a,b )
LIN b,e2,d
by A8, ANALMETR:40;
then A9:
b,e2 // b,d
by ANALMETR:def 10;
then A10:
a,c _|_ b,d
by A5, A6, ANALMETR:62;
then A11:
d,b _|_ a,c
by ANALMETR:61;
LIN a,e1,d
by A7, ANALMETR:40;
then A12:
a,e1 // a,d
by ANALMETR:def 10;
then A13:
b,c _|_ a,d
by A3, A4, ANALMETR:62;
then A14:
d,a _|_ b,c
by ANALMETR:61;
A15:
X is satisfying_LIN1
by A1, Th3;
A16:
now ( d <> c implies ( d,a _|_ b,c & d,b _|_ a,c & d,c _|_ a,b ) )assume A17:
d <> c
;
( d,a _|_ b,c & d,b _|_ a,c & d,c _|_ a,b )now ( b <> d implies ( d,a _|_ b,c & d,b _|_ a,c & d,c _|_ a,b ) )assume A18:
b <> d
;
( d,a _|_ b,c & d,b _|_ a,c & d,c _|_ a,b )
not
b9,
d9 // a9,
c9
proof
assume
b9,
d9 // a9,
c9
;
contradiction
then
a9,
c9 // b9,
d9
by AFF_1:4;
then A19:
a,
c // b,
d
by ANALMETR:36;
a <> c
then
b,
d _|_ b,
d
by A10, A19, ANALMETR:62;
hence
contradiction
by A18, ANALMETR:39;
verum
end; then consider o9 being
Element of
AffinStruct(# the
U1 of
X, the
CONGR of
X #)
such that A20:
LIN b9,
d9,
o9
and A21:
LIN a9,
c9,
o9
by AFF_1:60;
reconsider o =
o9 as
Element of
X ;
now ( d <> a implies ( d,a _|_ b,c & d,b _|_ a,c & d,c _|_ a,b ) )assume A22:
d <> a
;
( d,a _|_ b,c & d,b _|_ a,c & d,c _|_ a,b )A23:
o <> a
proof
assume A24:
o = a
;
contradiction
then
LIN b,
d,
a
by A20, ANALMETR:40;
then
b,
d // b,
a
by ANALMETR:def 10;
then
b,
a _|_ a,
c
by A10, A18, ANALMETR:62;
then A25:
a,
b _|_ a,
c
by ANALMETR:61;
LIN a9,
b9,
d9
by A20, A24, AFF_1:6;
then
LIN a,
b,
d
by ANALMETR:40;
then A26:
a,
b // a,
d
by ANALMETR:def 10;
a <> b
then
a,
d _|_ a,
c
by A25, A26, ANALMETR:62;
then
d,
a _|_ a,
c
by ANALMETR:61;
then
a,
c // b,
c
by A14, A22, ANALMETR:63;
then
c,
a // c,
b
by ANALMETR:59;
then
LIN c,
a,
b
by ANALMETR:def 10;
then
LIN c9,
a9,
b9
by ANALMETR:40;
then
LIN a9,
b9,
c9
by AFF_1:6;
hence
contradiction
by A2, ANALMETR:40;
verum
end; A27:
c <> o
proof
assume A28:
c = o
;
contradiction
then
LIN b,
d,
c
by A20, ANALMETR:40;
then
b,
d // b,
c
by ANALMETR:def 10;
then A29:
b,
c _|_ a,
c
by A10, A18, ANALMETR:62;
b <> c
then
a,
d // a,
c
by A13, A29, ANALMETR:63;
then
LIN a,
d,
c
by ANALMETR:def 10;
then
LIN a9,
d9,
c9
by ANALMETR:40;
then
LIN c9,
d9,
a9
by AFF_1:6;
then
LIN c,
d,
a
by ANALMETR:40;
then A30:
c,
d // c,
a
by ANALMETR:def 10;
LIN c9,
d9,
b9
by A20, A28, AFF_1:6;
then
LIN c,
d,
b
by ANALMETR:40;
then
c,
d // c,
b
by ANALMETR:def 10;
then
c,
a // c,
b
by A17, A30, ANALMETR:60;
then
LIN c,
a,
b
by ANALMETR:def 10;
then
LIN c9,
a9,
b9
by ANALMETR:40;
then
LIN a9,
b9,
c9
by AFF_1:6;
hence
contradiction
by A2, ANALMETR:40;
verum
end; consider e1 being
Element of
X such that A31:
a,
c // a,
e1
and A32:
a <> e1
by ANALMETR:39;
consider e2 being
Element of
X such that A33:
b,
c // d,
e2
and A34:
d <> e2
by ANALMETR:39;
reconsider e19 =
e1,
e29 =
e2 as
Element of
AffinStruct(# the
U1 of
X, the
CONGR of
X #) ;
not
a9,
e19 // d9,
e29
proof
assume
a9,
e19 // d9,
e29
;
contradiction
then
a,
e1 // d,
e2
by ANALMETR:36;
then
d,
e2 // a,
c
by A31, A32, ANALMETR:60;
then
a,
c // b,
c
by A33, A34, ANALMETR:60;
then
c,
a // c,
b
by ANALMETR:59;
then
LIN c,
a,
b
by ANALMETR:def 10;
then
LIN c9,
a9,
b9
by ANALMETR:40;
then
LIN a9,
b9,
c9
by AFF_1:6;
hence
contradiction
by A2, ANALMETR:40;
verum
end; then consider d19 being
Element of
AffinStruct(# the
U1 of
X, the
CONGR of
X #)
such that A35:
LIN a9,
e19,
d19
and A36:
LIN d9,
e29,
d19
by AFF_1:60;
reconsider d1 =
d19 as
Element of
X ;
LIN a,
e1,
d1
by A35, ANALMETR:40;
then
a,
e1 // a,
d1
by ANALMETR:def 10;
then A37:
a,
c // a,
d1
by A31, A32, ANALMETR:60;
then A38:
LIN a,
c,
d1
by ANALMETR:def 10;
LIN d,
e2,
d1
by A36, ANALMETR:40;
then
d,
e2 // d,
d1
by ANALMETR:def 10;
then A39:
b,
c // d,
d1
by A33, A34, ANALMETR:60;
A40:
o <> d
proof
assume A41:
o = d
;
contradiction
then A42:
a,
o _|_ b,
c
by A3, A4, A12, ANALMETR:62;
LIN a,
c,
o
by A21, ANALMETR:40;
then
a,
c // a,
o
by ANALMETR:def 10;
then A43:
a,
c _|_ b,
c
by A23, A42, ANALMETR:62;
a <> c
then
b,
o // b,
c
by A10, A41, A43, ANALMETR:63;
then
LIN b,
o,
c
by ANALMETR:def 10;
then
LIN b9,
o9,
c9
by ANALMETR:40;
then
LIN c9,
o9,
b9
by AFF_1:6;
then
LIN c,
o,
b
by ANALMETR:40;
then A44:
c,
o // c,
b
by ANALMETR:def 10;
LIN c9,
o9,
a9
by A21, AFF_1:6;
then
LIN c,
o,
a
by ANALMETR:40;
then
c,
o // c,
a
by ANALMETR:def 10;
then
c,
b // c,
a
by A27, A44, ANALMETR:60;
then
LIN c,
b,
a
by ANALMETR:def 10;
then
LIN c9,
b9,
a9
by ANALMETR:40;
then
LIN a9,
b9,
c9
by AFF_1:6;
hence
contradiction
by A2, ANALMETR:40;
verum
end; A45:
o <> d1
proof
assume A46:
o = d1
;
contradiction
LIN o9,
d9,
b9
by A20, AFF_1:6;
then
LIN o,
d,
b
by ANALMETR:40;
then
o,
d // o,
b
by ANALMETR:def 10;
then
d,
o // b,
o
by ANALMETR:59;
then
b,
c // b,
o
by A39, A40, A46, ANALMETR:60;
then
LIN b,
c,
o
by ANALMETR:def 10;
then
LIN b9,
c9,
o9
by ANALMETR:40;
then
LIN c9,
o9,
b9
by AFF_1:6;
then
LIN c,
o,
b
by ANALMETR:40;
then A47:
c,
o // c,
b
by ANALMETR:def 10;
LIN c9,
o9,
a9
by A21, AFF_1:6;
then
LIN c,
o,
a
by ANALMETR:40;
then
c,
o // c,
a
by ANALMETR:def 10;
then
c,
a // c,
b
by A27, A47, ANALMETR:60;
then
LIN c,
a,
b
by ANALMETR:def 10;
then
LIN c9,
a9,
b9
by ANALMETR:40;
then
LIN a9,
b9,
c9
by AFF_1:6;
hence
contradiction
by A2, ANALMETR:40;
verum
end; A48:
o <> b
A49:
d1 <> c
proof
assume A50:
d1 = c
;
contradiction
A51:
b <> c
c,
b // c,
d
by A39, A50, ANALMETR:59;
then
LIN c,
b,
d
by ANALMETR:def 10;
then A52:
LIN c9,
b9,
d9
by ANALMETR:40;
b,
c // c,
d
by A39, A50, ANALMETR:59;
then
d,
a _|_ c,
d
by A14, A51, ANALMETR:62;
then A53:
d,
c _|_ d,
a
by ANALMETR:61;
LIN d9,
c9,
b9
by A52, AFF_1:6;
then
LIN d,
c,
b
by ANALMETR:40;
then
d,
c // d,
b
by ANALMETR:def 10;
then
d,
b _|_ d,
a
by A17, A53, ANALMETR:62;
then
a,
c // d,
a
by A11, A18, ANALMETR:63;
then
a,
c // a,
d
by ANALMETR:59;
then
LIN a,
c,
d
by ANALMETR:def 10;
then
LIN a9,
c9,
d9
by ANALMETR:40;
then
LIN c9,
a9,
d9
by AFF_1:6;
then
LIN c,
a,
d
by ANALMETR:40;
then A54:
c,
a // c,
d
by ANALMETR:def 10;
c,
d // b,
c
by A39, A50, ANALMETR:59;
then
c,
a // b,
c
by A17, A54, ANALMETR:60;
then
c,
a // c,
b
by ANALMETR:59;
then
LIN c,
a,
b
by ANALMETR:def 10;
then
LIN c9,
a9,
b9
by ANALMETR:40;
then
LIN a9,
b9,
c9
by AFF_1:6;
hence
contradiction
by A2, ANALMETR:40;
verum
end;
LIN d9,
o9,
b9
by A20, AFF_1:6;
then
d9,
o9 // d9,
b9
by AFF_1:def 1;
then
b9,
d9 // o9,
d9
by AFF_1:4;
then
b,
d // o,
d
by ANALMETR:36;
then A55:
a,
c _|_ o,
d
by A10, A18, ANALMETR:62;
LIN a,
c,
o
by A21, ANALMETR:40;
then
a,
c // a,
o
by ANALMETR:def 10;
then A56:
a,
c // o,
a
by ANALMETR:59;
a <> c
then A57:
o,
d _|_ o,
a
by A55, A56, ANALMETR:62;
LIN a,
c,
o
by A21, ANALMETR:40;
then A58:
a,
c // a,
o
by ANALMETR:def 10;
A59:
a <> c
then
a,
o // a,
d1
by A37, A58, ANALMETR:60;
then
LIN a,
o,
d1
by ANALMETR:def 10;
then
LIN a9,
o9,
d19
by ANALMETR:40;
then
LIN o9,
a9,
d19
by AFF_1:6;
then
LIN o,
a,
d1
by ANALMETR:40;
then A60:
o,
a // o,
d1
by ANALMETR:def 10;
LIN a,
c,
o
by A21, ANALMETR:40;
then
a,
c // a,
o
by ANALMETR:def 10;
then
o,
a // a,
c
by ANALMETR:59;
then
a,
c // o,
d1
by A23, A60, ANALMETR:60;
then A61:
b,
d _|_ o,
d1
by A10, A59, ANALMETR:62;
LIN d9,
o9,
b9
by A20, AFF_1:6;
then
LIN d,
o,
b
by ANALMETR:40;
then
d,
o // d,
b
by ANALMETR:def 10;
then
b,
d // o,
d
by ANALMETR:59;
then A62:
o,
d1 _|_ o,
d
by A18, A61, ANALMETR:62;
LIN c9,
o9,
a9
by A21, AFF_1:6;
then
c9,
o9 // c9,
a9
by AFF_1:def 1;
then
a9,
c9 // o9,
c9
by AFF_1:4;
then A63:
a,
c // o,
c
by ANALMETR:36;
a <> c
then A64:
b,
d _|_ o,
c
by A10, A63, ANALMETR:62;
b9,
d9 // b9,
o9
by A20, AFF_1:def 1;
then
b9,
d9 // o9,
b9
by AFF_1:4;
then
b,
d // o,
b
by ANALMETR:36;
then A65:
o,
c _|_ o,
b
by A18, A64, ANALMETR:62;
A66:
not
LIN o,
d,
d1
LIN a9,
c9,
d19
by A38, ANALMETR:40;
then
LIN c9,
d19,
a9
by AFF_1:6;
then
c9,
d19 // c9,
a9
by AFF_1:def 1;
then
a9,
c9 // c9,
d19
by AFF_1:4;
then A67:
a,
c // c,
d1
by ANALMETR:36;
A68:
a <> c
LIN c9,
a9,
o9
by A21, AFF_1:6;
then
c9,
a9 // c9,
o9
by AFF_1:def 1;
then
a9,
c9 // c9,
o9
by AFF_1:4;
then
a,
c // c,
o
by ANALMETR:36;
then
c,
d1 // c,
o
by A67, A68, ANALMETR:60;
then
LIN c,
d1,
o
by ANALMETR:def 10;
then
LIN c9,
d19,
o9
by ANALMETR:40;
then
LIN o9,
d19,
c9
by AFF_1:6;
then A69:
LIN o,
d1,
c
by ANALMETR:40;
LIN o9,
d9,
b9
by A20, AFF_1:6;
then A70:
LIN o,
d,
b
by ANALMETR:40;
A71:
d1,
d // c,
b
by A39, ANALMETR:59;
b <> c
then
d,
d1 _|_ a,
d
by A13, A39, ANALMETR:62;
then
d1,
d _|_ d,
a
by ANALMETR:61;
then
c,
d _|_ b,
a
by A15, A23, A27, A40, A45, A48, A49, A57, A62, A65, A66, A69, A70, A71;
hence
(
d,
a _|_ b,
c &
d,
b _|_ a,
c &
d,
c _|_ a,
b )
by A10, A13, ANALMETR:61;
verum end; hence
(
d,
a _|_ b,
c &
d,
b _|_ a,
c &
d,
c _|_ a,
b )
by A3, A4, A10, A12, ANALMETR:61, ANALMETR:62;
verum end; hence
(
d,
a _|_ b,
c &
d,
b _|_ a,
c &
d,
c _|_ a,
b )
by A5, A6, A9, A13, ANALMETR:61, ANALMETR:62;
verum end;
now ( d = c implies ( d,a _|_ b,c & d,b _|_ a,c & d,c _|_ a,b ) )assume
d = c
;
( d,a _|_ b,c & d,b _|_ a,c & d,c _|_ a,b )then
a,
b _|_ d,
c
by ANALMETR:39;
hence
(
d,
a _|_ b,
c &
d,
b _|_ a,
c &
d,
c _|_ a,
b )
by A10, A13, ANALMETR:61;
verum end;
hence
( d,a _|_ b,c & d,b _|_ a,c & d,c _|_ a,b )
by A16; verum