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 ; CONAFFM:def 6 for a, a1, b, b1, c, c1 being Element of 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 ; ( 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 a' = a, a1' = a1, b' = b, b1' = b1, c' = c, c1' = c1, o' = o as Element of by ANALMETR:47;
now
ex
b2 being
Element of st
(
LIN o,
a1,
b2 &
c1,
b2 _|_ b,
c &
c1 <> b2 )
proof
consider y being
Element of
such that A15:
o,
a1 // o,
y
and A16:
o <> y
by ANALMETR:51;
consider x being
Element of
such that A17:
b,
c _|_ c1,
x
and A18:
c1 <> x
by ANALMETR:51;
A19:
not
o,
y // c1,
x
proof
assume A20:
o,
y // c1,
x
;
contradiction
reconsider y' =
y,
x' =
x as
Element of
by ANALMETR:47;
A21:
o',
y' // c1',
x'
by A20, ANALMETR:48;
o',
a1' // o',
y'
by A15, ANALMETR:48;
then
o',
y' // o',
a1'
by AFF_1:13;
then
c1',
x' // o',
a1'
by A16, A21, DIRAF:47;
then
c1,
x // o,
a1
by ANALMETR:48;
then
o,
a1 _|_ b,
c
by A17, A18, ANALMETR:84;
then A22:
o,
a // b,
c
by A3, A9, ANALMETR:85;
o,
a // o,
b
by A11, ANALMETR:def 11;
then
b,
c // o,
b
by A2, A22, ANALMETR:82;
then
b',
c' // o',
b'
by ANALMETR:48;
then
b',
c' // b',
o'
by AFF_1:13;
then
LIN b',
c',
o'
by AFF_1:def 1;
then
LIN o',
b',
c'
by AFF_1:15;
then A23:
o',
b' // o',
c'
by AFF_1:def 1;
LIN o',
a',
b'
by A11, ANALMETR:55;
then
LIN o',
b',
a'
by AFF_1:15;
then
o',
b' // o',
a'
by AFF_1:def 1;
then
o',
c' // o',
a'
by A4, A23, DIRAF:47;
then
LIN o',
c',
a'
by AFF_1:def 1;
hence
contradiction
by A10, ANALMETR:55;
verum
end;
reconsider y' =
y,
x' =
x as
Element of
by ANALMETR:47;
not
o',
y' // c1',
x'
by A19, ANALMETR:48;
then consider b2' being
Element of
such that A24:
LIN o',
y',
b2'
and A25:
LIN c1',
x',
b2'
by AFF_1:74;
reconsider b2 =
b2' as
Element of
by ANALMETR:47;
LIN c1,
x,
b2
by A25, ANALMETR:55;
then
c1,
x // c1,
b2
by ANALMETR:def 11;
then A26:
c1,
b2 _|_ b,
c
by A17, A18, ANALMETR:84;
o',
a1' // o',
y'
by A15, ANALMETR:48;
then A27:
o',
y' // o',
a1'
by AFF_1:13;
o',
y' // o',
b2'
by A24, AFF_1:def 1;
then
o',
a1' // o',
b2'
by A16, A27, DIRAF:47;
then
LIN o',
a1',
b2'
by AFF_1:def 1;
then A28:
LIN o,
a1,
b2
by ANALMETR:55;
c1 <> b2
proof
assume
c1 = b2
;
contradiction
then
o,
a1 // o,
c1
by A28, ANALMETR:def 11;
then
o,
c1 _|_ o,
a
by A3, A9, ANALMETR:84;
then
o,
c // o,
a
by A6, A8, ANALMETR:85;
hence
contradiction
by A10, ANALMETR:def 11;
verum
end;
hence
ex
b2 being
Element of st
(
LIN o,
a1,
b2 &
c1,
b2 _|_ b,
c &
c1 <> b2 )
by A26, A28;
verum
end; then consider b2 being
Element of
such that A29:
LIN o,
a1,
b2
and A30:
c1,
b2 _|_ b,
c
and
c1 <> b2
;
reconsider b2' =
b2 as
Element of
by ANALMETR:47;
o,
a1 // o,
b2
by A29, ANALMETR:def 11;
then A31:
o,
a _|_ o,
b2
by A3, A9, ANALMETR:84;
A32:
o,
a // o,
b
by A11, ANALMETR:def 11;
A33:
o <> b2
proof
assume
o = b2
;
contradiction
then
o,
c1 _|_ b,
c
by A30, ANALMETR:83;
then
o,
c // b,
c
by A6, A8, ANALMETR:85;
then
o',
c' // b',
c'
by ANALMETR:48;
then
c',
o' // c',
b'
by AFF_1:13;
then
LIN c',
o',
b'
by AFF_1:def 1;
then
LIN o',
b',
c'
by AFF_1:15;
then A34:
o',
b' // o',
c'
by AFF_1:def 1;
LIN o',
a',
b'
by A11, ANALMETR:55;
then
LIN o',
b',
a'
by AFF_1:15;
then
o',
b' // o',
a'
by AFF_1:def 1;
then
o',
c' // o',
a'
by A4, A34, DIRAF:47;
then
LIN o',
c',
a'
by AFF_1:def 1;
hence
contradiction
by A10, ANALMETR:55;
verum
end; A35:
o,
b _|_ o,
b2
by A2, A31, A32, ANALMETR:84;
b,
c _|_ b2,
c1
by A30, ANALMETR:83;
then A36:
a,
a1 // b,
b2
by A1, A2, A3, A4, A5, A6, A7, A8, A9, A10, A11, A13, A29, A33, A35, Def5;
not
LIN o,
a,
a1
then A37:
not
LIN o',
a',
a1'
by ANALMETR:55;
A38:
LIN o',
a',
b'
by A11, ANALMETR:55;
A39:
LIN o',
a1',
b1'
by A12, ANALMETR:55;
A40:
LIN o',
a1',
b2'
by A29, ANALMETR:55;
A41:
a',
a1' // b',
b1'
by A14, ANALMETR:48;
a',
a1' // b',
b2'
by A36, ANALMETR:48;
then
b1 = b2
by A37, A38, A39, A40, A41, AFF_1:70;
hence
b,
c _|_ b1,
c1
by A30, ANALMETR:83;
verum
hence
b,c _|_ b1,c1
; verum