let X be OrtAfPl; ( X is satisfying_LIN implies X is satisfying_LIN1 )
assume A1:
X is satisfying_LIN
; X is satisfying_LIN1
let o be Element of X; CONAFFM:def 6 for a, a1, b, b1, c, c1 being Element of X st o <> a & o <> a1 & o <> b & o <> b1 & o <> c & o <> c1 & a <> b & o,c _|_ o,c1 & o,a _|_ o,a1 & o,b _|_ o,b1 & not LIN o,c,a & LIN o,a,b & LIN o,a1,b1 & a,c _|_ a1,c1 & a,a1 // b,b1 holds
b,c _|_ b1,c1
let a, a1, b, b1, c, c1 be Element of X; ( o <> a & o <> a1 & o <> b & o <> b1 & o <> c & o <> c1 & a <> b & o,c _|_ o,c1 & o,a _|_ o,a1 & o,b _|_ o,b1 & not LIN o,c,a & LIN o,a,b & LIN o,a1,b1 & a,c _|_ a1,c1 & a,a1 // b,b1 implies b,c _|_ b1,c1 )
assume that
A2:
o <> a
and
A3:
o <> a1
and
A4:
o <> b
and
o <> b1
and
A5:
o <> c
and
A6:
o <> c1
and
A7:
a <> b
and
A8:
o,c _|_ o,c1
and
A9:
o,a _|_ o,a1
and
o,b _|_ o,b1
and
A10:
not LIN o,c,a
and
A11:
LIN o,a,b
and
A12:
LIN o,a1,b1
and
A13:
a,c _|_ a1,c1
and
A14:
a,a1 // b,b1
; b,c _|_ b1,c1
reconsider a9 = a, a19 = a1, b9 = b, b19 = b1, c9 = c, c19 = c1, o9 = o as Element of AffinStruct(# the U1 of X, the CONGR of X #) ;
now b,c _|_ b1,c1
ex
b2 being
Element of
X st
(
LIN o,
a1,
b2 &
c1,
b2 _|_ b,
c &
c1 <> b2 )
proof
consider y being
Element of
X such that A15:
o,
a1 // o,
y
and A16:
o <> y
by ANALMETR:39;
consider x being
Element of
X such that A17:
b,
c _|_ c1,
x
and A18:
c1 <> x
by ANALMETR:39;
A19:
not
o,
y // c1,
x
proof
assume A20:
o,
y // c1,
x
;
contradiction
reconsider y9 =
y,
x9 =
x as
Element of
AffinStruct(# the
U1 of
X, the
CONGR of
X #) ;
A21:
o9,
y9 // c19,
x9
by A20, ANALMETR:36;
o9,
a19 // o9,
y9
by A15, ANALMETR:36;
then
o9,
y9 // o9,
a19
by AFF_1:4;
then
c19,
x9 // o9,
a19
by A16, A21, DIRAF:40;
then
c1,
x // o,
a1
by ANALMETR:36;
then
o,
a1 _|_ b,
c
by A17, A18, ANALMETR:62;
then A22:
o,
a // b,
c
by A3, A9, ANALMETR:63;
o,
a // o,
b
by A11, ANALMETR:def 10;
then
b,
c // o,
b
by A2, A22, ANALMETR:60;
then
b9,
c9 // o9,
b9
by ANALMETR:36;
then
b9,
c9 // b9,
o9
by AFF_1:4;
then
LIN b9,
c9,
o9
by AFF_1:def 1;
then
LIN o9,
b9,
c9
by AFF_1:6;
then A23:
o9,
b9 // o9,
c9
by AFF_1:def 1;
LIN o9,
a9,
b9
by A11, ANALMETR:40;
then
LIN o9,
b9,
a9
by AFF_1:6;
then
o9,
b9 // o9,
a9
by AFF_1:def 1;
then
o9,
c9 // o9,
a9
by A4, A23, DIRAF:40;
then
LIN o9,
c9,
a9
by AFF_1:def 1;
hence
contradiction
by A10, ANALMETR:40;
verum
end;
reconsider y9 =
y,
x9 =
x as
Element of
AffinStruct(# the
U1 of
X, the
CONGR of
X #) ;
not
o9,
y9 // c19,
x9
by A19, ANALMETR:36;
then consider b29 being
Element of
AffinStruct(# the
U1 of
X, the
CONGR of
X #)
such that A24:
LIN o9,
y9,
b29
and A25:
LIN c19,
x9,
b29
by AFF_1:60;
reconsider b2 =
b29 as
Element of
X ;
LIN c1,
x,
b2
by A25, ANALMETR:40;
then
c1,
x // c1,
b2
by ANALMETR:def 10;
then A26:
c1,
b2 _|_ b,
c
by A17, A18, ANALMETR:62;
o9,
a19 // o9,
y9
by A15, ANALMETR:36;
then A27:
o9,
y9 // o9,
a19
by AFF_1:4;
o9,
y9 // o9,
b29
by A24, AFF_1:def 1;
then
o9,
a19 // o9,
b29
by A16, A27, DIRAF:40;
then
LIN o9,
a19,
b29
by AFF_1:def 1;
then A28:
LIN o,
a1,
b2
by ANALMETR:40;
c1 <> b2
proof
assume
c1 = b2
;
contradiction
then
o,
a1 // o,
c1
by A28, ANALMETR:def 10;
then
o,
c1 _|_ o,
a
by A3, A9, ANALMETR:62;
then
o,
c // o,
a
by A6, A8, ANALMETR:63;
hence
contradiction
by A10, ANALMETR:def 10;
verum
end;
hence
ex
b2 being
Element of
X st
(
LIN o,
a1,
b2 &
c1,
b2 _|_ b,
c &
c1 <> b2 )
by A26, A28;
verum
end; then consider b2 being
Element of
X such that A29:
LIN o,
a1,
b2
and A30:
c1,
b2 _|_ b,
c
and
c1 <> b2
;
reconsider b29 =
b2 as
Element of
AffinStruct(# the
U1 of
X, the
CONGR of
X #) ;
o,
a1 // o,
b2
by A29, ANALMETR:def 10;
then A31:
o,
a _|_ o,
b2
by A3, A9, ANALMETR:62;
A32:
o,
a // o,
b
by A11, ANALMETR:def 10;
A33:
o <> b2
proof
assume
o = b2
;
contradiction
then
o,
c1 _|_ b,
c
by A30, ANALMETR:61;
then
o,
c // b,
c
by A6, A8, ANALMETR:63;
then
o9,
c9 // b9,
c9
by ANALMETR:36;
then
c9,
o9 // c9,
b9
by AFF_1:4;
then
LIN c9,
o9,
b9
by AFF_1:def 1;
then
LIN o9,
b9,
c9
by AFF_1:6;
then A34:
o9,
b9 // o9,
c9
by AFF_1:def 1;
LIN o9,
a9,
b9
by A11, ANALMETR:40;
then
LIN o9,
b9,
a9
by AFF_1:6;
then
o9,
b9 // o9,
a9
by AFF_1:def 1;
then
o9,
c9 // o9,
a9
by A4, A34, DIRAF:40;
then
LIN o9,
c9,
a9
by AFF_1:def 1;
hence
contradiction
by A10, ANALMETR:40;
verum
end; A35:
o,
b _|_ o,
b2
by A2, A31, A32, ANALMETR:62;
b,
c _|_ b2,
c1
by A30, ANALMETR:61;
then A36:
a,
a1 // b,
b2
by A1, A2, A3, A4, A5, A6, A7, A8, A9, A10, A11, A13, A29, A33, A35;
not
LIN o,
a,
a1
then A37:
not
LIN o9,
a9,
a19
by ANALMETR:40;
A38:
LIN o9,
a9,
b9
by A11, ANALMETR:40;
A39:
LIN o9,
a19,
b19
by A12, ANALMETR:40;
A40:
LIN o9,
a19,
b29
by A29, ANALMETR:40;
A41:
a9,
a19 // b9,
b19
by A14, ANALMETR:36;
a9,
a19 // b9,
b29
by A36, ANALMETR:36;
then
b1 = b2
by A37, A38, A39, A40, A41, AFF_1:56;
hence
b,
c _|_ b1,
c1
by A30, ANALMETR:61;
verum
hence
b,c _|_ b1,c1
; verum