let X be OrtAfPl; :: thesis: ( X is satisfying_LIN implies X is satisfying_LIN1 )
assume A1:
X is satisfying_LIN
; :: thesis: X is satisfying_LIN1
let o be Element of X; :: according to CONAFFM:def 6 :: thesis: 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; :: thesis: ( 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 A2:
( 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 )
; :: thesis: b,c _|_ b1,c1
reconsider a' = a, a1' = a1, b' = b, b1' = b1, c' = c, c1' = c1, o' = o as Element of (Af X) by ANALMETR:47;
now
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 A3:
(
o,
a1 // o,
y &
o <> y )
by ANALMETR:51;
consider x being
Element of
X such that A4:
(
b,
c _|_ c1,
x &
c1 <> x )
by ANALMETR:51;
A5:
not
o,
y // c1,
x
proof
assume A6:
o,
y // c1,
x
;
:: thesis: contradiction
reconsider y' =
y,
x' =
x as
Element of
(Af X) by ANALMETR:47;
A7:
o',
y' // c1',
x'
by A6, ANALMETR:48;
(
o',
a1' // o',
y' &
o' <> y' )
by A3, ANALMETR:48;
then
(
o',
y' // o',
a1' &
o' <> y' )
by AFF_1:13;
then
c1',
x' // o',
a1'
by A7, DIRAF:47;
then
c1,
x // o,
a1
by ANALMETR:48;
then
o,
a1 _|_ b,
c
by A4, ANALMETR:84;
then A8:
o,
a // b,
c
by A2, ANALMETR:85;
o,
a // o,
b
by A2, ANALMETR:def 11;
then
b,
c // o,
b
by A2, A8, 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 A9:
o',
b' // o',
c'
by AFF_1:def 1;
(
LIN o',
a',
b' &
o' <> b' )
by A2, ANALMETR:55;
then
(
LIN o',
b',
a' &
o' <> b' )
by AFF_1:15;
then
(
o',
b' // o',
a' &
o' <> b' )
by AFF_1:def 1;
then
o',
c' // o',
a'
by A9, DIRAF:47;
then
LIN o',
c',
a'
by AFF_1:def 1;
hence
contradiction
by A2, ANALMETR:55;
:: thesis: verum
end;
reconsider y' =
y,
x' =
x as
Element of
(Af X) by ANALMETR:47;
not
o',
y' // c1',
x'
by A5, ANALMETR:48;
then consider b2' being
Element of
(Af X) such that A10:
(
LIN o',
y',
b2' &
LIN c1',
x',
b2' )
by AFF_1:74;
reconsider b2 =
b2' as
Element of
X by ANALMETR:47;
LIN c1,
x,
b2
by A10, ANALMETR:55;
then
c1,
x // c1,
b2
by ANALMETR:def 11;
then A11:
c1,
b2 _|_ b,
c
by A4, ANALMETR:84;
(
o',
a1' // o',
y' &
o' <> y' )
by A3, ANALMETR:48;
then A12:
(
o',
y' // o',
a1' &
o' <> y' )
by AFF_1:13;
o',
y' // o',
b2'
by A10, AFF_1:def 1;
then
o',
a1' // o',
b2'
by A12, DIRAF:47;
then
LIN o',
a1',
b2'
by AFF_1:def 1;
then A13:
LIN o,
a1,
b2
by ANALMETR:55;
c1 <> b2
proof
assume
c1 = b2
;
:: thesis: contradiction
then
o,
a1 // o,
c1
by A13, ANALMETR:def 11;
then
o,
c1 _|_ o,
a
by A2, ANALMETR:84;
then
o,
c // o,
a
by A2, ANALMETR:85;
hence
contradiction
by A2, ANALMETR:def 11;
:: thesis: verum
end;
hence
ex
b2 being
Element of
X st
(
LIN o,
a1,
b2 &
c1,
b2 _|_ b,
c &
c1 <> b2 )
by A11, A13;
:: thesis: verum
end; then consider b2 being
Element of
X such that A14:
(
LIN o,
a1,
b2 &
c1,
b2 _|_ b,
c &
c1 <> b2 )
;
reconsider b2' =
b2 as
Element of
(Af X) by ANALMETR:47;
A15:
(
o,
b _|_ o,
b2 &
o <> b2 )
proof
A16:
o,
b _|_ o,
b2
proof
o,
a1 // o,
b2
by A14, ANALMETR:def 11;
then A17:
o,
a _|_ o,
b2
by A2, ANALMETR:84;
o,
a // o,
b
by A2, ANALMETR:def 11;
hence
o,
b _|_ o,
b2
by A2, A17, ANALMETR:84;
:: thesis: verum
end;
o <> b2
proof
assume
o = b2
;
:: thesis: contradiction
then
o,
c1 _|_ b,
c
by A14, ANALMETR:83;
then
o,
c // b,
c
by A2, 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 A18:
o',
b' // o',
c'
by AFF_1:def 1;
(
LIN o',
a',
b' &
o' <> b' )
by A2, ANALMETR:55;
then
(
LIN o',
b',
a' &
o' <> b' )
by AFF_1:15;
then
(
o',
b' // o',
a' &
o' <> b' )
by AFF_1:def 1;
then
o',
c' // o',
a'
by A18, DIRAF:47;
then
LIN o',
c',
a'
by AFF_1:def 1;
hence
contradiction
by A2, ANALMETR:55;
:: thesis: verum
end;
hence
(
o,
b _|_ o,
b2 &
o <> b2 )
by A16;
:: thesis: verum
end;
b,
c _|_ b2,
c1
by A14, ANALMETR:83;
then A19:
a,
a1 // b,
b2
by A1, A2, A14, A15, Def5;
b1 = b2
proof
not
LIN o,
a,
a1
then A20:
not
LIN o',
a',
a1'
by ANALMETR:55;
A21:
LIN o',
a',
b'
by A2, ANALMETR:55;
A22:
LIN o',
a1',
b1'
by A2, ANALMETR:55;
A23:
LIN o',
a1',
b2'
by A14, ANALMETR:55;
A24:
a',
a1' // b',
b1'
by A2, ANALMETR:48;
a',
a1' // b',
b2'
by A19, ANALMETR:48;
hence
b1 = b2
by A20, A21, A22, A23, A24, AFF_1:70;
:: thesis: verum
end; hence
b,
c _|_ b1,
c1
by A14, ANALMETR:83;
:: thesis: verum
hence
b,c _|_ b1,c1
; :: thesis: verum