:: CONAFFM semantic presentation

begin


definition
let X be OrtAfPl;
attrX is satisfying_DES  means :: CONAFFM:def 1
 for o, a, a1, b, b1, c, c1 being Element of X st o <> a & o <> a1 & o <> b & o <> b1 & o <> c & o <> c1 & not LIN b,b1,a & not LIN a,a1,c & LIN o,a,a1 & LIN o,b,b1 & LIN o,c,c1 & a,b // a1,b1 & a,c // a1,c1 holds
b,c // b1,c1;
attrX is satisfying_AH  means :: CONAFFM:def 2
 for o, 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 _|_ a1,b1 & o,a // b,c & a,c _|_ a1,c1 & not o,c // o,a & not o,a // o,b holds
b,c _|_ b1,c1;
attrX is satisfying_3H  means :: CONAFFM:def 3
 for a, 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 );
attrX is satisfying_ODES  means :Def4: :: CONAFFM:def 4
 for o, 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 _|_ a1,b1 & a,c _|_ a1,c1 & not o,c // o,a & not o,a // o,b holds
b,c _|_ b1,c1;
attrX is satisfying_LIN  means :Def5: :: CONAFFM:def 5
 for o, 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 & b,c _|_ b1,c1 holds
a,a1 // b,b1;
attrX is satisfying_LIN1  means :Def6: :: CONAFFM:def 6
 for o, 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;
attrX is satisfying_LIN2  means :: CONAFFM:def 7
 for o, 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 & a,a1 // b,b1 & 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 & b,c _|_ b1,c1 holds
o,c _|_ o,c1;
end;

:: deftheorem  defines satisfying_DES CONAFFM:def_1_:_
 for X being OrtAfPl holds
( X is satisfying_DES iff for o, a, a1, b, b1, c, c1 being Element of X st o <> a & o <> a1 & o <> b & o <> b1 & o <> c & o <> c1 & not LIN b,b1,a & not LIN a,a1,c & LIN o,a,a1 & LIN o,b,b1 & LIN o,c,c1 & a,b // a1,b1 & a,c // a1,c1 holds
b,c // b1,c1 );

:: deftheorem  defines satisfying_AH CONAFFM:def_2_:_
 for X being OrtAfPl holds
( X is satisfying_AH iff for o, 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 _|_ a1,b1 & o,a // b,c & a,c _|_ a1,c1 & not o,c // o,a & not o,a // o,b holds
b,c _|_ b1,c1 );

:: deftheorem  defines satisfying_3H CONAFFM:def_3_:_
 for X being OrtAfPl holds
( X is satisfying_3H iff for a, 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 ) );

:: deftheorem Def4 defines satisfying_ODES CONAFFM:def_4_:_
 for X being OrtAfPl holds
( X is satisfying_ODES iff for o, 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 _|_ a1,b1 & a,c _|_ a1,c1 & not o,c // o,a & not o,a // o,b holds
b,c _|_ b1,c1 );

:: deftheorem Def5 defines satisfying_LIN CONAFFM:def_5_:_
 for X being OrtAfPl holds
( X is satisfying_LIN iff for o, 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 & b,c _|_ b1,c1 holds
a,a1 // b,b1 );

:: deftheorem Def6 defines satisfying_LIN1 CONAFFM:def_6_:_
 for X being OrtAfPl holds
( X is satisfying_LIN1 iff for o, 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 );

:: deftheorem  defines satisfying_LIN2 CONAFFM:def_7_:_
 for X being OrtAfPl holds
( X is satisfying_LIN2 iff for o, 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 & a,a1 // b,b1 & 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 & b,c _|_ b1,c1 holds
o,c _|_ o,c1 );

theorem :: CONAFFM:1
for X being OrtAfPl st X is satisfying_ODES holds
X is satisfying_DES
proof
let X be OrtAfPl; ::_thesis: ( X is satisfying_ODES implies X is satisfying_DES )
assume A1: X is satisfying_ODES ; ::_thesis: X is satisfying_DES
let o be Element of X; :: according to CONAFFM:def_1 ::_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 & not LIN b,b1,a & not LIN a,a1,c & LIN o,a,a1 & LIN o,b,b1 & LIN o,c,c1 & a,b // a1,b1 & a,c // a1,c1 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 & not LIN b,b1,a & not LIN a,a1,c & LIN o,a,a1 & LIN o,b,b1 & LIN o,c,c1 & a,b // a1,b1 & a,c // a1,c1 implies b,c // b1,c1 )
assume that
A2: o <> a and
A3: o <> a1 and
A4: o <> b and
A5: o <> b1 and
A6: o <> c and
 o <> c1 and
A7: not LIN b,b1,a and
A8: not LIN a,a1,c and
A9: LIN o,a,a1 and
A10: LIN o,b,b1 and
A11: LIN o,c,c1 and
A12: a,b // a1,b1 and
A13: a,c // a1,c1 ; ::_thesis: b,c // b1,c1
consider a2 being Element of X such that
A14: o,a _|_ o,a2 and
A15: o <> a2 by ANALMETR:def_9;
consider e1 being Element of X such that
A16: o,b _|_ o,e1 and
A17: o <> e1 by ANALMETR:def_9;
consider e2 being Element of X such that
A18: a,b _|_ a2,e2 and
A19: a2 <> e2 by ANALMETR:def_9;
reconsider o9 = o, a9 = a, a19 = a1, b9 = b, b19 = b1, c9 = c, c19 = c1, a29 = a2, e19 = e1, e29 = e2 as Element of (Af X) by ANALMETR:35;
 not o9,e19 // a29,e29
proof
assume  o9,e19 // a29,e29 ; ::_thesis: contradiction
then  o,e1 // a2,e2 by ANALMETR:36;
then  a2,e2 _|_ o,b by A16, A17, ANALMETR:62;
then  a,b // o,b by A18, A19, ANALMETR:63;
then A20: a9,b9 // o9,b9 by ANALMETR:36;
then  b9,a9 // b9,o9 by AFF_1:4;
then A21: LIN b9,a9,o9 by AFF_1:def_1;
 o9,b9 // b9,a9 by A20, AFF_1:4;
then A22: o,b // b,a by ANALMETR:36;
A23: b9 <> a9
proof
assume  b9 = a9 ; ::_thesis: contradiction
then  LIN b9,b19,a9 by AFF_1:7;
hence  contradiction by A7, ANALMETR:40; ::_thesis: verum
end;
 o,b // o,b1 by A10, ANALMETR:def_10;
then  b,a // o,b1 by A4, A22, ANALMETR:60;
then  b9,a9 // o9,b19 by ANALMETR:36;
then  LIN b9,a9,b19 by A21, A23, AFF_1:9;
then  LIN b9,b19,a9 by AFF_1:6;
hence  contradiction by A7, ANALMETR:40; ::_thesis: verum
end;
then consider b29 being Element of (Af X) such that
A24: LIN o9,e19,b29 and
A25: LIN a29,e29,b29 by AFF_1:60;
reconsider b2 = b29 as Element of X by ANALMETR:35;
 LIN o,e1,b2 by A24, ANALMETR:40;
then  o,e1 // o,b2 by ANALMETR:def_10;
then A26: o,b _|_ o,b2 by A16, A17, ANALMETR:62;
 LIN a2,e2,b2 by A25, ANALMETR:40;
then  a2,e2 // a2,b2 by ANALMETR:def_10;
then A27: a,b _|_ a2,b2 by A18, A19, ANALMETR:62;
consider e1 being Element of X such that
A28: o,c _|_ o,e1 and
A29: o <> e1 by ANALMETR:def_9;
consider e2 being Element of X such that
A30: a,c _|_ a2,e2 and
A31: a2 <> e2 by ANALMETR:def_9;
reconsider e19 = e1, e29 = e2 as Element of (Af X) by ANALMETR:35;
 not o9,e19 // a29,e29
proof
assume  o9,e19 // a29,e29 ; ::_thesis: contradiction
then  o,e1 // a2,e2 by ANALMETR:36;
then  o,c _|_ a2,e2 by A28, A29, ANALMETR:62;
then  o,c // a,c by A30, A31, ANALMETR:63;
then  c,o // c,a by ANALMETR:59;
then  LIN c,o,a by ANALMETR:def_10;
then  LIN c9,o9,a9 by ANALMETR:40;
then  LIN a9,c9,o9 by AFF_1:6;
then  LIN a,c,o by ANALMETR:40;
then  a,c // a,o by ANALMETR:def_10;
then A32: o,a // a,c by ANALMETR:59;
 LIN o9,a9,a19 by A9, ANALMETR:40;
then  LIN a9,o9,a19 by AFF_1:6;
then  LIN a,o,a1 by ANALMETR:40;
then  a,o // a,a1 by ANALMETR:def_10;
then  o,a // a,a1 by ANALMETR:59;
then  a,a1 // a,c by A2, A32, ANALMETR:60;
hence  contradiction by A8, ANALMETR:def_10; ::_thesis: verum
end;
then consider c29 being Element of (Af X) such that
A33: LIN o9,e19,c29 and
A34: LIN a29,e29,c29 by AFF_1:60;
reconsider c2 = c29 as Element of X by ANALMETR:35;
 LIN o,e1,c2 by A33, ANALMETR:40;
then  o,e1 // o,c2 by ANALMETR:def_10;
then A35: o,c _|_ o,c2 by A28, A29, ANALMETR:62;
 LIN a2,e2,c2 by A34, ANALMETR:40;
then  a2,e2 // a2,c2 by ANALMETR:def_10;
then A36: a,c _|_ a2,c2 by A30, A31, ANALMETR:62;
A37: not o,c // o,a
proof
assume  o,c // o,a ; ::_thesis: contradiction
then  LIN o,c,a by ANALMETR:def_10;
then  LIN o9,c9,a9 by ANALMETR:40;
then  LIN a9,o9,c9 by AFF_1:6;
then  LIN a,o,c by ANALMETR:40;
then A38: a,o // a,c by ANALMETR:def_10;
 LIN o9,a9,a19 by A9, ANALMETR:40;
then  LIN a9,o9,a19 by AFF_1:6;
then  LIN a,o,a1 by ANALMETR:40;
then  a,o // a,a1 by ANALMETR:def_10;
then  a,a1 // a,c by A2, A38, ANALMETR:60;
hence  contradiction by A8, ANALMETR:def_10; ::_thesis: verum
end;
 not o,a // o,b
proof
assume  o,a // o,b ; ::_thesis: contradiction
then  LIN o,a,b by ANALMETR:def_10;
then  LIN o9,a9,b9 by ANALMETR:40;
then  LIN b9,o9,a9 by AFF_1:6;
then  LIN b,o,a by ANALMETR:40;
then A39: b,o // b,a by ANALMETR:def_10;
 LIN o9,b9,b19 by A10, ANALMETR:40;
then  LIN b9,o9,b19 by AFF_1:6;
then  LIN b,o,b1 by ANALMETR:40;
then  b,o // b,b1 by ANALMETR:def_10;
then  b,b1 // b,a by A4, A39, ANALMETR:60;
hence  contradiction by A7, ANALMETR:def_10; ::_thesis: verum
end;
then A40: b,c _|_ b2,c2 by A1, A14, A26, A27, A35, A36, A37, Def4;
 o,a // o,a1 by A9, ANALMETR:def_10;
then A41: o,a1 _|_ o,a2 by A2, A14, ANALMETR:62;
 o,b // o,b1 by A10, ANALMETR:def_10;
then A42: o,b1 _|_ o,b2 by A4, A26, ANALMETR:62;
 o,c // o,c1 by A11, ANALMETR:def_10;
then A43: o,c1 _|_ o,c2 by A6, A35, ANALMETR:62;
 a <> b
proof
assume  a = b ; ::_thesis: contradiction
then  LIN b9,b19,a9 by AFF_1:7;
hence  contradiction by A7, ANALMETR:40; ::_thesis: verum
end;
then A44: a1,b1 _|_ a2,b2 by A12, A27, ANALMETR:62;
 a <> c
proof
assume  a = c ; ::_thesis: contradiction
then  LIN a9,a19,c9 by AFF_1:7;
hence  contradiction by A8, ANALMETR:40; ::_thesis: verum
end;
then A45: a1,c1 _|_ a2,c2 by A13, A36, ANALMETR:62;
A46: not o,c1 // o,a1
proof
assume  o,c1 // o,a1 ; ::_thesis: contradiction
then  LIN o,c1,a1 by ANALMETR:def_10;
then  LIN o9,c19,a19 by ANALMETR:40;
then  LIN a19,o9,c19 by AFF_1:6;
then  LIN a1,o,c1 by ANALMETR:40;
then A47: a1,o // a1,c1 by ANALMETR:def_10;
A48: a1 <> c1
proof
assume  a1 = c1 ; ::_thesis: contradiction
then  LIN o9,c9,a19 by A11, ANALMETR:40;
then  LIN a19,c9,o9 by AFF_1:6;
then  LIN a1,c,o by ANALMETR:40;
then A49: a1,c // a1,o by ANALMETR:def_10;
 LIN o9,a9,a19 by A9, ANALMETR:40;
then  LIN a19,o9,a9 by AFF_1:6;
then  LIN a1,o,a by ANALMETR:40;
then  a1,o // a1,a by ANALMETR:def_10;
then  a1,c // a1,a by A3, A49, ANALMETR:60;
then  LIN a1,c,a by ANALMETR:def_10;
then  LIN a19,c9,a9 by ANALMETR:40;
then  LIN a9,a19,c9 by AFF_1:6;
hence  contradiction by A8, ANALMETR:40; ::_thesis: verum
end;
 LIN o9,a9,a19 by A9, ANALMETR:40;
then  LIN a19,o9,a9 by AFF_1:6;
then  LIN a1,o,a by ANALMETR:40;
then  a1,o // a1,a by ANALMETR:def_10;
then  a1,c1 // a1,a by A3, A47, ANALMETR:60;
then  a1,a // a,c by A13, A48, ANALMETR:60;
then  a,a1 // a,c by ANALMETR:59;
hence  contradiction by A8, ANALMETR:def_10; ::_thesis: verum
end;
 not o,a1 // o,b1
proof
assume  o,a1 // o,b1 ; ::_thesis: contradiction
then  LIN o,a1,b1 by ANALMETR:def_10;
then  LIN o9,a19,b19 by ANALMETR:40;
then  LIN b19,a19,o9 by AFF_1:6;
then  LIN b1,a1,o by ANALMETR:40;
then A50: b1,a1 // b1,o by ANALMETR:def_10;
A51: a1 <> b1
proof
assume  a1 = b1 ; ::_thesis: contradiction
then  LIN o9,a9,b19 by A9, ANALMETR:40;
then  LIN b19,o9,a9 by AFF_1:6;
then  LIN b1,o,a by ANALMETR:40;
then A52: b1,o // b1,a by ANALMETR:def_10;
 LIN o9,b9,b19 by A10, ANALMETR:40;
then  LIN b19,b9,o9 by AFF_1:6;
then  LIN b1,b,o by ANALMETR:40;
then  b1,b // b1,o by ANALMETR:def_10;
then  b1,a // b1,b by A5, A52, ANALMETR:60;
then  LIN b1,a,b by ANALMETR:def_10;
then  LIN b19,a9,b9 by ANALMETR:40;
then  LIN b9,b19,a9 by AFF_1:6;
hence  contradiction by A7, ANALMETR:40; ::_thesis: verum
end;
A53: b1,a1 // a,b by A12, ANALMETR:59;
 LIN o9,b9,b19 by A10, ANALMETR:40;
then  LIN b19,b9,o9 by AFF_1:6;
then  LIN b1,b,o by ANALMETR:40;
then  b1,b // b1,o by ANALMETR:def_10;
then  b1,a1 // b1,b by A5, A50, ANALMETR:60;
then  b1,b // a,b by A51, A53, ANALMETR:60;
then  b,b1 // b,a by ANALMETR:59;
hence  contradiction by A7, ANALMETR:def_10; ::_thesis: verum
end;
then A54: b1,c1 _|_ b2,c2 by A1, A41, A42, A43, A44, A45, A46, Def4;
A55: now__::_thesis:_(_not_LIN_o,b,c_implies_b,c_//_b1,c1_)
assume A56: not LIN o,b,c ; ::_thesis: b,c // b1,c1
 b2 <> c2
proof
assume A57: b2 = c2 ; ::_thesis: contradiction
 o <> b2
proof
assume A58: o = b2 ; ::_thesis: contradiction
 a2,o _|_ a,o by A14, ANALMETR:61;
then  a,o // a,b by A15, A27, A58, ANALMETR:63;
then  LIN a,o,b by ANALMETR:def_10;
then  LIN a9,o9,b9 by ANALMETR:40;
then  LIN b9,o9,a9 by AFF_1:6;
then  LIN b,o,a by ANALMETR:40;
then A59: b,o // b,a by ANALMETR:def_10;
 LIN o9,b9,b19 by A10, ANALMETR:40;
then  LIN b9,o9,b19 by AFF_1:6;
then  LIN b,o,b1 by ANALMETR:40;
then  b,o // b,b1 by ANALMETR:def_10;
then  b,b1 // b,a by A4, A59, ANALMETR:60;
hence  contradiction by A7, ANALMETR:def_10; ::_thesis: verum
end;
then  o,b // o,c by A26, A35, A57, ANALMETR:63;
hence  contradiction by A56, ANALMETR:def_10; ::_thesis: verum
end;
hence  b,c // b1,c1 by A40, A54, ANALMETR:63; ::_thesis: verum
end;
now__::_thesis:_(_LIN_o,b,c_implies_b,c_//_b1,c1_)
assume A60: LIN o,b,c ; ::_thesis: b,c // b1,c1
then  LIN o9,b9,c9 by ANALMETR:40;
then  LIN b9,o9,c9 by AFF_1:6;
then A61: b9,o9 // b9,c9 by AFF_1:def_1;
 LIN o9,b9,b19 by A10, ANALMETR:40;
then  LIN b9,o9,b19 by AFF_1:6;
then  b9,o9 // b9,b19 by AFF_1:def_1;
then  b9,c9 // b9,b19 by A4, A61, AFF_1:5;
then A62: LIN b9,c9,b19 by AFF_1:def_1;
 LIN o9,b9,c9 by A60, ANALMETR:40;
then  LIN c9,o9,b9 by AFF_1:6;
then A63: c9,o9 // c9,b9 by AFF_1:def_1;
 LIN o9,c9,c19 by A11, ANALMETR:40;
then  LIN c9,o9,c19 by AFF_1:6;
then  c9,o9 // c9,c19 by AFF_1:def_1;
then  c9,b9 // c9,c19 by A6, A63, AFF_1:5;
then  LIN c9,b9,c19 by AFF_1:def_1;
then  LIN b9,c9,c19 by AFF_1:6;
then  b9,c9 // b19,c19 by A62, AFF_1:10;
hence  b,c // b1,c1 by ANALMETR:36; ::_thesis: verum
end;
hence  b,c // b1,c1 by A55; ::_thesis: verum
end;

theorem :: CONAFFM:2
for X being OrtAfPl st X is satisfying_ODES holds
X is satisfying_AH
proof
let X be OrtAfPl; ::_thesis: ( X is satisfying_ODES implies X is satisfying_AH )
assume A1: X is satisfying_ODES ; ::_thesis: X is satisfying_AH
let o be Element of X; :: according to CONAFFM:def_2 ::_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 _|_ a1,b1 & o,a // b,c & a,c _|_ a1,c1 & not o,c // o,a & not o,a // o,b 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 _|_ a1,b1 & o,a // b,c & a,c _|_ a1,c1 & not o,c // o,a & not o,a // o,b implies b,c _|_ b1,c1 )
assume that
A2: o,a _|_ o,a1 and
A3: o,b _|_ o,b1 and
A4: o,c _|_ o,c1 and
A5: a,b _|_ a1,b1 and
 o,a // b,c and
A6: a,c _|_ a1,c1 and
A7: not o,c // o,a and
A8: not o,a // o,b ; ::_thesis: b,c _|_ b1,c1
thus  b,c _|_ b1,c1 by A1, A2, A3, A4, A5, A6, A7, A8, Def4; ::_thesis: verum
end;

theorem Th3: :: CONAFFM:3
for X being OrtAfPl st X is satisfying_LIN holds
X is satisfying_LIN1
proof
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 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 ; ::_thesis: b,c _|_ b1,c1
reconsider a9 = a, a19 = a1, b9 = b, b19 = b1, c9 = c, c19 = c1, o9 = o as Element of (Af X) by ANALMETR:35;
now__::_thesis:_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 ; ::_thesis: contradiction
reconsider y9 = y, x9 = x as Element of (Af X) by ANALMETR:35;
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; ::_thesis: verum
end;
reconsider y9 = y, x9 = x as Element of (Af X) by ANALMETR:35;
 not o9,y9 // c19,x9 by A19, ANALMETR:36;
then consider b29 being Element of (Af 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 by ANALMETR:35;
 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 ; ::_thesis: 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; ::_thesis: verum
end;
hence  ex b2 being Element of X st
( LIN o,a1,b2 & c1,b2 _|_ b,c & c1 <> b2 ) by A26, A28; ::_thesis: 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 (Af X) by ANALMETR:35;
 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 ; ::_thesis: 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; ::_thesis: 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, Def5;
 not LIN o,a,a1
proof
assume  LIN o,a,a1 ; ::_thesis: contradiction
then  o,a // o,a1 by ANALMETR:def_10;
then  o,a1 _|_ o,a1 by A2, A9, ANALMETR:62;
hence  contradiction by A3, ANALMETR:39; ::_thesis: verum
end;
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; ::_thesis: verum
end;
hence  b,c _|_ b1,c1 ; ::_thesis: verum
end;

theorem :: CONAFFM:4
for X being OrtAfPl st X is satisfying_LIN1 holds
X is satisfying_LIN2
proof
let X be OrtAfPl; ::_thesis: ( X is satisfying_LIN1 implies X is satisfying_LIN2 )
assume A1: X is satisfying_LIN1 ; ::_thesis: X is satisfying_LIN2
let o be Element of X; :: according to CONAFFM:def_7 ::_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 & a,a1 // b,b1 & 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 & b,c _|_ b1,c1 holds
o,c _|_ o,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 & a,a1 // b,b1 & 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 & b,c _|_ b1,c1 implies o,c _|_ o,c1 )
assume that
A2: o <> a and
A3: o <> a1 and
A4: o <> b and
A5: o <> b1 and
A6: o <> c and
 o <> c1 and
A7: a <> b and
A8: a,a1 // b,b1 and
A9: o,a _|_ o,a1 and
A10: o,b _|_ o,b1 and
A11: not LIN o,c,a and
A12: LIN o,a,b and
A13: LIN o,a1,b1 and
A14: a,c _|_ a1,c1 and
A15: b,c _|_ b1,c1 ; ::_thesis: o,c _|_ o,c1
reconsider a9 = a, a19 = a1, b9 = b, b19 = b1, c9 = c, c19 = c1, o9 = o as Element of (Af X) by ANALMETR:35;
 ex c2 being Element of X st
( LIN a1,c1,c2 & o,c _|_ o,c2 & o <> c2 )
proof
consider e1 being Element of X such that
A16: a1,c1 // a1,e1 and
A17: a1 <> e1 by ANALMETR:39;
consider e2 being Element of X such that
A18: o,c _|_ o,e2 and
A19: o <> e2 by ANALMETR:39;
reconsider e19 = e1, e29 = e2 as Element of (Af X) by ANALMETR:35;
 not a19,e19 // o9,e29
proof
assume  a19,e19 // o9,e29 ; ::_thesis: contradiction
then  a1,e1 // o,e2 by ANALMETR:36;
then  a1,c1 // o,e2 by A16, A17, ANALMETR:60;
then A20: a1,c1 _|_ o,c by A18, A19, ANALMETR:62;
 a1 <> c1
proof
assume A21: a1 = c1 ; ::_thesis: contradiction
A22: b1 <> a1
proof
assume  b1 = a1 ; ::_thesis: contradiction
then  a1,a // a1,b by A8, ANALMETR:59;
then  LIN a1,a,b by ANALMETR:def_10;
then  LIN a19,a9,b9 by ANALMETR:40;
then  LIN a9,b9,a19 by AFF_1:6;
then  LIN a,b,a1 by ANALMETR:40;
then A23: a,b // a,a1 by ANALMETR:def_10;
 LIN o9,a9,b9 by A12, ANALMETR:40;
then  LIN a9,b9,o9 by AFF_1:6;
then  LIN a,b,o by ANALMETR:40;
then  a,b // a,o by ANALMETR:def_10;
then  o,a // a,b by ANALMETR:59;
then  a,a1 // o,a by A7, A23, ANALMETR:60;
then  a,a1 // a,o by ANALMETR:59;
then  LIN a,a1,o by ANALMETR:def_10;
then  LIN a9,a19,o9 by ANALMETR:40;
then  LIN o9,a9,a19 by AFF_1:6;
then  LIN o,a,a1 by ANALMETR:40;
then  o,a // o,a1 by ANALMETR:def_10;
then  o,a _|_ o,a by A3, A9, ANALMETR:62;
hence  contradiction by A2, ANALMETR:39; ::_thesis: verum
end;
A24: LIN o9,a9,b9 by A12, ANALMETR:40;
A25: LIN o9,a19,b19 by A13, ANALMETR:40;
A26: LIN b9,o9,a9 by A24, AFF_1:6;
A27: LIN b19,o9,a19 by A25, AFF_1:6;
A28: LIN b,o,a by A26, ANALMETR:40;
A29: LIN b1,o,a1 by A27, ANALMETR:40;
A30: b,o // b,a by A28, ANALMETR:def_10;
A31: b1,o // b1,a1 by A29, ANALMETR:def_10;
 b,o _|_ b1,o by A10, ANALMETR:61;
then  b,a _|_ b1,o by A4, A30, ANALMETR:62;
then  b1,a1 _|_ b,a by A5, A31, ANALMETR:62;
then  b,c // b,a by A15, A21, A22, ANALMETR:63;
then  LIN b,c,a by ANALMETR:def_10;
then  LIN b9,c9,a9 by ANALMETR:40;
then  LIN a9,b9,c9 by AFF_1:6;
then  LIN a,b,c by ANALMETR:40;
then A32: a,b // a,c by ANALMETR:def_10;
 LIN o9,a9,b9 by A12, ANALMETR:40;
then  LIN a9,b9,o9 by AFF_1:6;
then  LIN a,b,o by ANALMETR:40;
then  a,b // a,o by ANALMETR:def_10;
then  a,c // a,o by A7, A32, ANALMETR:60;
then  LIN a,c,o by ANALMETR:def_10;
then  LIN a9,c9,o9 by ANALMETR:40;
then  LIN o9,c9,a9 by AFF_1:6;
hence  contradiction by A11, ANALMETR:40; ::_thesis: verum
end;
then  a,c // o,c by A14, A20, ANALMETR:63;
then  c,a // c,o by ANALMETR:59;
then  c9,a9 // c9,o9 by ANALMETR:36;
then  LIN c9,a9,o9 by AFF_1:def_1;
then  LIN o9,c9,a9 by AFF_1:6;
hence  contradiction by A11, ANALMETR:40; ::_thesis: verum
end;
then consider c29 being Element of (Af X) such that
A33: LIN a19,e19,c29 and
A34: LIN o9,e29,c29 by AFF_1:60;
reconsider c2 = c29 as Element of X by ANALMETR:35;
take  c2 ; ::_thesis: ( LIN a1,c1,c2 & o,c _|_ o,c2 & o <> c2 )
 a19,e19 // a19,c29 by A33, AFF_1:def_1;
then  a1,e1 // a1,c2 by ANALMETR:36;
then A35: a1,c1 // a1,c2 by A16, A17, ANALMETR:60;
 LIN o,e2,c2 by A34, ANALMETR:40;
then A36: o,e2 // o,c2 by ANALMETR:def_10;
 o <> c2
proof
assume  o = c2 ; ::_thesis: contradiction
then  a1,c1 // o,a1 by A35, ANALMETR:59;
then A37: o,a _|_ a1,c1 by A3, A9, ANALMETR:62;
 a1 <> c1
proof
assume A38: a1 = c1 ; ::_thesis: contradiction
A39: a1 <> b1
proof
assume  a1 = b1 ; ::_thesis: contradiction
then  a1,a // a1,b by A8, ANALMETR:59;
then  LIN a1,a,b by ANALMETR:def_10;
then  LIN a19,a9,b9 by ANALMETR:40;
then  LIN a9,b9,a19 by AFF_1:6;
then  LIN a,b,a1 by ANALMETR:40;
then A40: a,b // a,a1 by ANALMETR:def_10;
 LIN o9,a9,b9 by A12, ANALMETR:40;
then  LIN a9,b9,o9 by AFF_1:6;
then  LIN a,b,o by ANALMETR:40;
then  a,b // a,o by ANALMETR:def_10;
then  o,a // a,b by ANALMETR:59;
then  a,a1 // o,a by A7, A40, ANALMETR:60;
then  a,a1 // a,o by ANALMETR:59;
then  LIN a,a1,o by ANALMETR:def_10;
then  LIN a9,a19,o9 by ANALMETR:40;
then  LIN o9,a9,a19 by AFF_1:6;
then  LIN o,a,a1 by ANALMETR:40;
then  o,a // o,a1 by ANALMETR:def_10;
then  o,a _|_ o,a by A3, A9, ANALMETR:62;
hence  contradiction by A2, ANALMETR:39; ::_thesis: verum
end;
 LIN o9,a19,b19 by A13, ANALMETR:40;
then  LIN b19,a19,o9 by AFF_1:6;
then  LIN b1,a1,o by ANALMETR:40;
then  b1,a1 // b1,o by ANALMETR:def_10;
then  b1,a1 // o,b1 by ANALMETR:59;
then  b,c _|_ o,b1 by A15, A38, A39, ANALMETR:62;
then A41: b,c // o,b by A5, A10, ANALMETR:63;
A42: LIN o9,a9,b9 by A12, ANALMETR:40;
then A43: LIN b9,a9,o9 by AFF_1:6;
A44: LIN a9,b9,o9 by A42, AFF_1:6;
A45: LIN b,a,o by A43, ANALMETR:40;
A46: LIN a,b,o by A44, ANALMETR:40;
A47: b,a // b,o by A45, ANALMETR:def_10;
A48: a,b // a,o by A46, ANALMETR:def_10;
 o,b // b,a by A47, ANALMETR:59;
then  b,a // b,c by A4, A41, ANALMETR:60;
then  LIN b,a,c by ANALMETR:def_10;
then  LIN b9,a9,c9 by ANALMETR:40;
then  LIN a9,b9,c9 by AFF_1:6;
then  LIN a,b,c by ANALMETR:40;
then  a,b // a,c by ANALMETR:def_10;
then  a,o // a,c by A7, A48, ANALMETR:60;
then  LIN a,o,c by ANALMETR:def_10;
then  LIN a9,o9,c9 by ANALMETR:40;
then  LIN o9,c9,a9 by AFF_1:6;
hence  contradiction by A11, ANALMETR:40; ::_thesis: verum
end;
then  o,a // a,c by A14, A37, ANALMETR:63;
then  a,c // a,o by ANALMETR:59;
then  LIN a,c,o by ANALMETR:def_10;
then  LIN a9,c9,o9 by ANALMETR:40;
then  LIN o9,c9,a9 by AFF_1:6;
hence  contradiction by A11, ANALMETR:40; ::_thesis: verum
end;
hence  ( LIN a1,c1,c2 & o,c _|_ o,c2 & o <> c2 ) by A18, A19, A35, A36, ANALMETR:62, ANALMETR:def_10; ::_thesis: verum
end;
then consider c2 being Element of X such that
A49: LIN a1,c1,c2 and
A50: o,c _|_ o,c2 and
A51: o <> c2 ;
reconsider c29 = c2 as Element of (Af X) by ANALMETR:35;
A52: ( b <> c & a1 <> b1 & a1 <> c1 )
proof
assume A53: ( b = c or a1 = b1 or a1 = c1 ) ; ::_thesis: contradiction
A54: now__::_thesis:_not_b_=_c
assume  b = c ; ::_thesis: contradiction
then  LIN o9,a9,c9 by A12, ANALMETR:40;
then  LIN o9,c9,a9 by AFF_1:6;
hence  contradiction by A11, ANALMETR:40; ::_thesis: verum
end;
A55: now__::_thesis:_not_a1_=_b1
assume  a1 = b1 ; ::_thesis: contradiction
then  a1,a // a1,b by A8, ANALMETR:59;
then  LIN a1,a,b by ANALMETR:def_10;
then  LIN a19,a9,b9 by ANALMETR:40;
then  LIN a9,b9,a19 by AFF_1:6;
then  LIN a,b,a1 by ANALMETR:40;
then A56: a,b // a,a1 by ANALMETR:def_10;
 LIN o9,a9,b9 by A12, ANALMETR:40;
then  LIN a9,b9,o9 by AFF_1:6;
then  LIN a,b,o by ANALMETR:40;
then  a,b // a,o by ANALMETR:def_10;
then  o,a // a,b by ANALMETR:59;
then  a,a1 // o,a by A7, A56, ANALMETR:60;
then  a,a1 // a,o by ANALMETR:59;
then  LIN a,a1,o by ANALMETR:def_10;
then  LIN a9,a19,o9 by ANALMETR:40;
then  LIN o9,a9,a19 by AFF_1:6;
then  LIN o,a,a1 by ANALMETR:40;
then  o,a // o,a1 by ANALMETR:def_10;
then  o,a _|_ o,a by A3, A9, ANALMETR:62;
hence  contradiction by A2, ANALMETR:39; ::_thesis: verum
end;
now__::_thesis:_not_a1_=_c1
assume A57: a1 = c1 ; ::_thesis: contradiction
 LIN o9,a19,b19 by A13, ANALMETR:40;
then  LIN b19,a19,o9 by AFF_1:6;
then  LIN b1,a1,o by ANALMETR:40;
then  b1,a1 // b1,o by ANALMETR:def_10;
then  b1,a1 // o,b1 by ANALMETR:59;
then  b,c _|_ o,b1 by A15, A55, A57, ANALMETR:62;
then A58: b,c // o,b by A5, A10, ANALMETR:63;
A59: LIN o9,a9,b9 by A12, ANALMETR:40;
then A60: LIN b9,a9,o9 by AFF_1:6;
A61: LIN a9,b9,o9 by A59, AFF_1:6;
A62: LIN b,a,o by A60, ANALMETR:40;
A63: LIN a,b,o by A61, ANALMETR:40;
A64: b,a // b,o by A62, ANALMETR:def_10;
A65: a,b // a,o by A63, ANALMETR:def_10;
 o,b // b,a by A64, ANALMETR:59;
then  b,a // b,c by A4, A58, ANALMETR:60;
then  LIN b,a,c by ANALMETR:def_10;
then  LIN b9,a9,c9 by ANALMETR:40;
then  LIN a9,b9,c9 by AFF_1:6;
then  LIN a,b,c by ANALMETR:40;
then  a,b // a,c by ANALMETR:def_10;
then  a,o // a,c by A7, A65, ANALMETR:60;
then  LIN a,o,c by ANALMETR:def_10;
then  LIN a9,o9,c9 by ANALMETR:40;
then  LIN o9,c9,a9 by AFF_1:6;
hence  contradiction by A11, ANALMETR:40; ::_thesis: verum
end;
hence  contradiction by A53, A54, A55; ::_thesis: verum
end;
 a1,c1 // a1,c2 by A49, ANALMETR:def_10;
then  a,c _|_ a1,c2 by A14, A52, ANALMETR:62;
then  b,c _|_ b1,c2 by A1, A2, A3, A4, A5, A6, A7, A8, A9, A10, A11, A12, A13, A50, A51, Def6;
then  b1,c1 // b1,c2 by A15, A52, ANALMETR:63;
then A66: LIN b1,c1,c2 by ANALMETR:def_10;
 not LIN b1,a1,c1
proof
assume  LIN b1,a1,c1 ; ::_thesis: contradiction
then  LIN b19,a19,c19 by ANALMETR:40;
then  LIN a19,b19,c19 by AFF_1:6;
then  a19,b19 // a19,c19 by AFF_1:def_1;
then A67: a1,b1 // a1,c1 by ANALMETR:36;
 LIN o9,a19,b19 by A13, ANALMETR:40;
then  LIN a19,b19,o9 by AFF_1:6;
then  LIN a1,b1,o by ANALMETR:40;
then  a1,b1 // a1,o by ANALMETR:def_10;
then  a1,c1 // a1,o by A52, A67, ANALMETR:60;
then  a,c _|_ a1,o by A14, A52, ANALMETR:62;
then A68: o,a1 _|_ a,c by ANALMETR:61;
 o,a1 _|_ a,o by A9, ANALMETR:61;
then  a,o // a,c by A3, A68, ANALMETR:63;
then  LIN a,o,c by ANALMETR:def_10;
then  LIN a9,o9,c9 by ANALMETR:40;
then  LIN o9,c9,a9 by AFF_1:6;
hence  contradiction by A11, ANALMETR:40; ::_thesis: verum
end;
then A69: not LIN b19,a19,c19 by ANALMETR:40;
A70: LIN b19,c19,c29 by A66, ANALMETR:40;
 a1,c1 // a1,c2 by A49, ANALMETR:def_10;
then  a19,c19 // a19,c29 by ANALMETR:36;
hence  o,c _|_ o,c1 by A50, A69, A70, AFF_1:14; ::_thesis: verum
end;

theorem :: CONAFFM:5
for X being OrtAfPl st X is satisfying_LIN holds
X is satisfying_ODES
proof
let X be OrtAfPl; ::_thesis: ( X is satisfying_LIN implies X is satisfying_ODES )
assume A1: X is satisfying_LIN ; ::_thesis: X is satisfying_ODES
let o be Element of X; :: according to CONAFFM:def_4 ::_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 _|_ a1,b1 & a,c _|_ a1,c1 & not o,c // o,a & not o,a // o,b 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 _|_ a1,b1 & a,c _|_ a1,c1 & not o,c // o,a & not o,a // o,b implies b,c _|_ b1,c1 )
assume that
A2: o,a _|_ o,a1 and
A3: o,b _|_ o,b1 and
A4: o,c _|_ o,c1 and
A5: a,b _|_ a1,b1 and
A6: a,c _|_ a1,c1 and
A7: not o,c // o,a and
A8: not o,a // o,b ; ::_thesis: b,c _|_ b1,c1
A9: X is satisfying_LIN1 by A1, Th3;
now__::_thesis:_for_o,_a,_a1,_b,_b1,_c,_c1_being_Element_of_X_st_X_is_satisfying_LIN_&_o,a__|__o,a1_&_o,b__|__o,b1_&_o,c__|__o,c1_&_a,b__|__a1,b1_&_a,c__|__a1,c1_&_not_o,c_//_o,a_&_not_o,a_//_o,b_&_not_o,b_//_a,c_holds_
b,c__|__b1,c1
let o, a, a1, b, b1, c, c1 be Element of X; ::_thesis: ( X is satisfying_LIN & o,a _|_ o,a1 & o,b _|_ o,b1 & o,c _|_ o,c1 & a,b _|_ a1,b1 & a,c _|_ a1,c1 & not o,c // o,a & not o,a // o,b & not o,b // a,c implies b,c _|_ b1,c1 )
assume A10: X is satisfying_LIN ; ::_thesis: ( o,a _|_ o,a1 & o,b _|_ o,b1 & o,c _|_ o,c1 & a,b _|_ a1,b1 & a,c _|_ a1,c1 & not o,c // o,a & not o,a // o,b & not o,b // a,c implies b,c _|_ b1,c1 )
assume that
A11: o,a _|_ o,a1 and
A12: o,b _|_ o,b1 and
A13: o,c _|_ o,c1 and
A14: a,b _|_ a1,b1 and
A15: a,c _|_ a1,c1 and
A16: not o,c // o,a and
A17: not o,a // o,b ; ::_thesis: ( not o,b // a,c implies b,c _|_ b1,c1 )
assume A18: not o,b // a,c ; ::_thesis: b,c _|_ b1,c1
reconsider a9 = a, a19 = a1, b9 = b, b19 = b1, c9 = c, c19 = c1, o9 = o as Element of (Af X) by ANALMETR:35;
A19: now__::_thesis:_(_o_=_a1_implies_b,c__|__b1,c1_)
assume A20: o = a1 ; ::_thesis: b,c _|_ b1,c1
then A21: a1,b1 _|_ b,a1 by A12, ANALMETR:61;
A22: a1,b1 _|_ b,a by A14, ANALMETR:61;
 not b,a1 // b,a
proof
assume  b,a1 // b,a ; ::_thesis: contradiction
then  LIN b,o,a by A20, ANALMETR:def_10;
then  LIN b9,o9,a9 by ANALMETR:40;
then  LIN o9,a9,b9 by AFF_1:6;
then  LIN o,a,b by ANALMETR:40;
hence  contradiction by A17, ANALMETR:def_10; ::_thesis: verum
end;
then A23: a1 = b1 by A21, A22, ANALMETR:63;
A24: a1,c1 _|_ c,a1 by A13, A20, ANALMETR:61;
 a1,c1 _|_ c,a by A15, ANALMETR:61;
then A25: ( c,a1 // c,a or a1 = c1 ) by A24, ANALMETR:63;
 not c,a1 // c,a
proof
assume  c,a1 // c,a ; ::_thesis: contradiction
then  LIN c,o,a by A20, ANALMETR:def_10;
then  LIN c9,o9,a9 by ANALMETR:40;
then  LIN o9,c9,a9 by AFF_1:6;
then  LIN o,c,a by ANALMETR:40;
hence  contradiction by A16, ANALMETR:def_10; ::_thesis: verum
end;
hence  b,c _|_ b1,c1 by A23, A25, ANALMETR:39; ::_thesis: verum
end;
A26: now__::_thesis:_(_LIN_o,b,c_&_o_<>_a1_implies_b,c__|__b1,c1_)
assume that
A27: LIN o,b,c and
A28: o <> a1 ; ::_thesis: b,c _|_ b1,c1
A29: o <> b by A17, ANALMETR:39;
A30: o <> c
proof
assume  o = c ; ::_thesis: contradiction
then  o,a // o,c by ANALMETR:39;
then  o9,a9 // o9,c9 by ANALMETR:36;
then  o9,c9 // o9,a9 by AFF_1:4;
hence  contradiction by A16, ANALMETR:36; ::_thesis: verum
end;
A31: o <> b1
proof
assume A32: o = b1 ; ::_thesis: contradiction
 a1,o _|_ a,o by A11, ANALMETR:61;
then  a,o // a,b by A14, A28, A32, ANALMETR:63;
then  LIN a,o,b by ANALMETR:def_10;
then  LIN a9,o9,b9 by ANALMETR:40;
then  LIN o9,a9,b9 by AFF_1:6;
then  LIN o,a,b by ANALMETR:40;
hence  contradiction by A17, ANALMETR:def_10; ::_thesis: verum
end;
 o,b // o,c by A27, ANALMETR:def_10;
then  o,c _|_ o,b1 by A12, A29, ANALMETR:62;
then  o,b1 // o,c1 by A13, A30, ANALMETR:63;
then  LIN o,b1,c1 by ANALMETR:def_10;
then  LIN o9,b19,c19 by ANALMETR:40;
then  LIN b19,o9,c19 by AFF_1:6;
then  LIN b1,o,c1 by ANALMETR:40;
then A33: b1,o // b1,c1 by ANALMETR:def_10;
 b1,o _|_ b,o by A12, ANALMETR:61;
then A34: b,o _|_ b1,c1 by A31, A33, ANALMETR:62;
 LIN o9,b9,c9 by A27, ANALMETR:40;
then  LIN b9,o9,c9 by AFF_1:6;
then  LIN b,o,c by ANALMETR:40;
then  b,o // b,c by ANALMETR:def_10;
hence  b,c _|_ b1,c1 by A29, A34, ANALMETR:62; ::_thesis: verum
end;
A35: now__::_thesis:_(_LIN_a,b,c_&_not_LIN_o,b,c_&_o_<>_a1_implies_b,c__|__b1,c1_)
assume that
A36: LIN a,b,c and
 not LIN o,b,c and
A37: o <> a1 ; ::_thesis: b,c _|_ b1,c1
A38: a <> c
proof
assume  a = c ; ::_thesis: contradiction
then  a,o // a,c by ANALMETR:39;
then  LIN a,o,c by ANALMETR:def_10;
then  LIN a9,o9,c9 by ANALMETR:40;
then  LIN o9,c9,a9 by AFF_1:6;
then  LIN o,c,a by ANALMETR:40;
hence  contradiction by A16, ANALMETR:def_10; ::_thesis: verum
end;
A39: a <> b
proof
assume  a = b ; ::_thesis: contradiction
then  a,o // a,b by ANALMETR:39;
then  LIN a,o,b by ANALMETR:def_10;
then  LIN a9,o9,b9 by ANALMETR:40;
then  LIN o9,a9,b9 by AFF_1:6;
then  LIN o,a,b by ANALMETR:40;
hence  contradiction by A17, ANALMETR:def_10; ::_thesis: verum
end;
A40: a1 <> b1 by A11, A12, A17, A37, ANALMETR:63;
 a,b // a,c by A36, ANALMETR:def_10;
then  a,c _|_ a1,b1 by A14, A39, ANALMETR:62;
then  a1,b1 // a1,c1 by A15, A38, ANALMETR:63;
then  LIN a1,b1,c1 by ANALMETR:def_10;
then  LIN a19,b19,c19 by ANALMETR:40;
then  LIN b19,a19,c19 by AFF_1:6;
then  LIN b1,a1,c1 by ANALMETR:40;
then A41: b1,a1 // b1,c1 by ANALMETR:def_10;
 b1,a1 _|_ b,a by A14, ANALMETR:61;
then A42: b,a _|_ b1,c1 by A40, A41, ANALMETR:62;
 LIN a9,b9,c9 by A36, ANALMETR:40;
then  LIN b9,a9,c9 by AFF_1:6;
then  LIN b,a,c by ANALMETR:40;
then  b,a // b,c by ANALMETR:def_10;
hence  b,c _|_ b1,c1 by A39, A42, ANALMETR:62; ::_thesis: verum
end;
now__::_thesis:_(_not_LIN_a,b,c_&_not_LIN_o,b,c_&_o_<>_a1_implies_b,c__|__b1,c1_)
assume that
A43: not LIN a,b,c and
A44: not LIN o,b,c and
A45: o <> a1 ; ::_thesis: b,c _|_ b1,c1
A46: o <> c
proof
assume  o = c ; ::_thesis: contradiction
then  o,a // o,c by ANALMETR:39;
then  o9,a9 // o9,c9 by ANALMETR:36;
then  o9,c9 // o9,a9 by AFF_1:4;
hence  contradiction by A16, ANALMETR:36; ::_thesis: verum
end;
A47: o <> b1
proof
assume A48: o = b1 ; ::_thesis: contradiction
 a1,o _|_ a,o by A11, ANALMETR:61;
then  a,o // a,b by A14, A45, A48, ANALMETR:63;
then  LIN a,o,b by ANALMETR:def_10;
then  LIN a9,o9,b9 by ANALMETR:40;
then  LIN o9,a9,b9 by AFF_1:6;
then  LIN o,a,b by ANALMETR:40;
hence  contradiction by A17, ANALMETR:def_10; ::_thesis: verum
end;
A49: o <> c1
proof
assume A50: o = c1 ; ::_thesis: contradiction
 a1,o _|_ a,o by A11, ANALMETR:61;
then  a,o // a,c by A15, A45, A50, ANALMETR:63;
then  LIN a,o,c by ANALMETR:def_10;
then  LIN a9,o9,c9 by ANALMETR:40;
then  LIN o9,c9,a9 by AFF_1:6;
then  LIN o,c,a by ANALMETR:40;
hence  contradiction by A16, ANALMETR:def_10; ::_thesis: verum
end;
A51: o <> a by A16, ANALMETR:39;
A52: o <> b by A17, ANALMETR:39;
A53: a <> c by A13, A16, A49, ANALMETR:63;
A54: a1 <> c1 by A11, A13, A16, A49, ANALMETR:63;
 ex e being Element of X st
( LIN o,e,b & LIN a,c,e & e <> c & e <> b )
proof
consider p being Element of X such that
A55: o,b // o,p and
A56: o <> p by ANALMETR:39;
reconsider p9 = p as Element of (Af X) by ANALMETR:35;
consider p1 being Element of X such that
A57: a,c // a,p1 and
A58: a <> p1 by ANALMETR:39;
reconsider p19 = p1 as Element of (Af X) by ANALMETR:35;
 not o,p // a,p1
proof
assume  o,p // a,p1 ; ::_thesis: contradiction
then  a,p1 // o,b by A55, A56, ANALMETR:60;
hence  contradiction by A18, A57, A58, ANALMETR:60; ::_thesis: verum
end;
then  not o9,p9 // a9,p19 by ANALMETR:36;
then consider e9 being Element of (Af X) such that
A59: LIN o9,p9,e9 and
A60: LIN a9,p19,e9 by AFF_1:60;
reconsider e = e9 as Element of X by ANALMETR:35;
 LIN o,p,e by A59, ANALMETR:40;
then  o,p // o,e by ANALMETR:def_10;
then  o,e // o,b by A55, A56, ANALMETR:60;
then A61: LIN o,e,b by ANALMETR:def_10;
 LIN a,p1,e by A60, ANALMETR:40;
then  a,p1 // a,e by ANALMETR:def_10;
then  a,c // a,e by A57, A58, ANALMETR:60;
then A62: LIN a,c,e by ANALMETR:def_10;
A63: c <> e
proof
assume  c = e ; ::_thesis: contradiction
then  LIN o9,c9,b9 by A61, ANALMETR:40;
then  LIN o9,b9,c9 by AFF_1:6;
hence  contradiction by A44, ANALMETR:40; ::_thesis: verum
end;
 b <> e
proof
assume  b = e ; ::_thesis: contradiction
then  LIN a9,c9,b9 by A62, ANALMETR:40;
then  LIN a9,b9,c9 by AFF_1:6;
hence  contradiction by A43, ANALMETR:40; ::_thesis: verum
end;
hence  ex e being Element of X st
( LIN o,e,b & LIN a,c,e & e <> c & e <> b ) by A61, A62, A63; ::_thesis: verum
end;
then consider e being Element of X such that
A64: LIN o,e,b and
A65: LIN a,c,e and
A66: e <> c and
A67: e <> b ;
reconsider e9 = e as Element of (Af X) by ANALMETR:35;
 ex e1 being Element of X st
( LIN o,e1,b1 & LIN a1,c1,e1 )
proof
consider p being Element of X such that
A68: o,b1 // o,p and
A69: o <> p by ANALMETR:39;
reconsider p9 = p as Element of (Af X) by ANALMETR:35;
consider p1 being Element of X such that
A70: a1,c1 // a1,p1 and
A71: a1 <> p1 by ANALMETR:39;
reconsider p19 = p1 as Element of (Af X) by ANALMETR:35;
A72: not o,b1 // a1,c1
proof
assume  o,b1 // a1,c1 ; ::_thesis: contradiction
then  a1,c1 _|_ o,b by A12, A47, ANALMETR:62;
hence  contradiction by A15, A18, A54, ANALMETR:63; ::_thesis: verum
end;
 not o,p // a1,p1
proof
assume  o,p // a1,p1 ; ::_thesis: contradiction
then  a1,p1 // o,b1 by A68, A69, ANALMETR:60;
hence  contradiction by A70, A71, A72, ANALMETR:60; ::_thesis: verum
end;
then  not o9,p9 // a19,p19 by ANALMETR:36;
then consider e19 being Element of (Af X) such that
A73: LIN o9,p9,e19 and
A74: LIN a19,p19,e19 by AFF_1:60;
reconsider e1 = e19 as Element of X by ANALMETR:35;
 LIN o,p,e1 by A73, ANALMETR:40;
then  o,p // o,e1 by ANALMETR:def_10;
then  o,e1 // o,b1 by A68, A69, ANALMETR:60;
then A75: LIN o,e1,b1 by ANALMETR:def_10;
 LIN a1,p1,e1 by A74, ANALMETR:40;
then  a1,p1 // a1,e1 by ANALMETR:def_10;
then  a1,c1 // a1,e1 by A70, A71, ANALMETR:60;
then  LIN a1,c1,e1 by ANALMETR:def_10;
hence  ex e1 being Element of X st
( LIN o,e1,b1 & LIN a1,c1,e1 ) by A75; ::_thesis: verum
end;
then consider e1 being Element of X such that
A76: LIN o,e1,b1 and
A77: LIN a1,c1,e1 ;
reconsider e19 = e1 as Element of (Af X) by ANALMETR:35;
 o,e // o,b by A64, ANALMETR:def_10;
then  o9,e9 // o9,b9 by ANALMETR:36;
then  o9,b9 // o9,e9 by AFF_1:4;
then  o,b // o,e by ANALMETR:36;
then A78: o,b1 _|_ o,e by A12, A52, ANALMETR:62;
 o,e1 // o,b1 by A76, ANALMETR:def_10;
then  o9,e19 // o9,b19 by ANALMETR:36;
then  o9,b19 // o9,e19 by AFF_1:4;
then A79: o,b1 // o,e1 by ANALMETR:36;
A80: o <> e
proof
assume  o = e ; ::_thesis: contradiction
then  LIN a9,c9,o9 by A65, ANALMETR:40;
then  LIN o9,c9,a9 by AFF_1:6;
then  LIN o,c,a by ANALMETR:40;
hence  contradiction by A16, ANALMETR:def_10; ::_thesis: verum
end;
A81: o <> e1
proof
assume  o = e1 ; ::_thesis: contradiction
then  LIN a19,c19,o9 by A77, ANALMETR:40;
then  LIN o9,a19,c19 by AFF_1:6;
then  LIN o,a1,c1 by ANALMETR:40;
then  o,a1 // o,c1 by ANALMETR:def_10;
then  o,c1 _|_ o,a by A11, A45, ANALMETR:62;
hence  contradiction by A13, A16, A49, ANALMETR:63; ::_thesis: verum
end;
A82: o,e _|_ o,e1 by A47, A78, A79, ANALMETR:62;
A83: not LIN o,a,e
proof
assume  LIN o,a,e ; ::_thesis: contradiction
then  o,a // o,e by ANALMETR:def_10;
then  o9,a9 // o9,e9 by ANALMETR:36;
then  o9,e9 // o9,a9 by AFF_1:4;
then A84: o,e // o,a by ANALMETR:36;
 o,e // o,b by A64, ANALMETR:def_10;
hence  contradiction by A17, A80, A84, ANALMETR:60; ::_thesis: verum
end;
 a,c // a,e by A65, ANALMETR:def_10;
then  a9,c9 // a9,e9 by ANALMETR:36;
then  a9,c9 // e9,a9 by AFF_1:4;
then  a,c // e,a by ANALMETR:36;
then A85: a1,c1 _|_ e,a by A15, A53, ANALMETR:62;
 a1,c1 // a1,e1 by A77, ANALMETR:def_10;
then  e,a _|_ a1,e1 by A54, A85, ANALMETR:62;
then A86: e,a _|_ e1,a1 by ANALMETR:61;
 b,a _|_ b1,a1 by A14, ANALMETR:61;
then A87: e,e1 // b,b1 by A10, A11, A12, A45, A47, A51, A52, A64, A67, A76, A80, A81, A82, A83, A86, Def5;
A88: not LIN o,c,e
proof
assume  LIN o,c,e ; ::_thesis: contradiction
then  LIN o9,c9,e9 by ANALMETR:40;
then  LIN c9,e9,o9 by AFF_1:6;
then  c9,e9 // c9,o9 by AFF_1:def_1;
then A89: c,e // c,o by ANALMETR:36;
 LIN a9,c9,e9 by A65, ANALMETR:40;
then  LIN c9,e9,a9 by AFF_1:6;
then  c9,e9 // c9,a9 by AFF_1:def_1;
then  c,e // c,a by ANALMETR:36;
then  c,o // c,a by A66, A89, ANALMETR:60;
then  LIN c,o,a by ANALMETR:def_10;
then  LIN c9,o9,a9 by ANALMETR:40;
then  LIN o9,c9,a9 by AFF_1:6;
then  LIN o,c,a by ANALMETR:40;
hence  contradiction by A16, ANALMETR:def_10; ::_thesis: verum
end;
 LIN a9,c9,e9 by A65, ANALMETR:40;
then  LIN c9,a9,e9 by AFF_1:6;
then  c9,a9 // c9,e9 by AFF_1:def_1;
then  a9,c9 // e9,c9 by AFF_1:4;
then  a,c // e,c by ANALMETR:36;
then A90: a1,c1 _|_ e,c by A15, A53, ANALMETR:62;
 LIN a19,c19,e19 by A77, ANALMETR:40;
then  LIN c19,a19,e19 by AFF_1:6;
then  c19,a19 // c19,e19 by AFF_1:def_1;
then  a19,c19 // e19,c19 by AFF_1:4;
then  a1,c1 // e1,c1 by ANALMETR:36;
then  e,c _|_ e1,c1 by A54, A90, ANALMETR:62;
hence  b,c _|_ b1,c1 by A9, A12, A13, A46, A47, A49, A52, A64, A67, A76, A80, A81, A82, A87, A88, Def6; ::_thesis: verum
end;
hence  b,c _|_ b1,c1 by A19, A26, A35; ::_thesis: verum
end;
then A91: ( not o,b // a,c implies b,c _|_ b1,c1 ) by A1, A2, A3, A4, A5, A6, A7, A8;
A92: now__::_thesis:_for_o,_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__|__a1,b1_&_a,c__|__a1,c1_&_not_o,c_//_o,a_&_not_o,a_//_o,b_&_not_o,a_//_c,b_holds_
b,c__|__b1,c1
let o, 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 _|_ a1,b1 & a,c _|_ a1,c1 & not o,c // o,a & not o,a // o,b & not o,a // c,b implies b,c _|_ b1,c1 )
assume that
A93: o,a _|_ o,a1 and
A94: o,b _|_ o,b1 and
A95: o,c _|_ o,c1 and
A96: a,b _|_ a1,b1 and
A97: a,c _|_ a1,c1 and
A98: not o,c // o,a and
A99: not o,a // o,b ; ::_thesis: ( not o,a // c,b implies b,c _|_ b1,c1 )
assume A100: not o,a // c,b ; ::_thesis: b,c _|_ b1,c1
reconsider a9 = a, a19 = a1, b9 = b, b19 = b1, c9 = c, c19 = c1, o9 = o as Element of (Af X) by ANALMETR:35;
A101: now__::_thesis:_(_o_=_a1_implies_b,c__|__b1,c1_)
assume A102: o = a1 ; ::_thesis: b,c _|_ b1,c1
then A103: a1,b1 _|_ b,a1 by A94, ANALMETR:61;
A104: a1,b1 _|_ b,a by A96, ANALMETR:61;
 not b,a1 // b,a
proof
assume  b,a1 // b,a ; ::_thesis: contradiction
then  LIN b,o,a by A102, ANALMETR:def_10;
then  LIN b9,o9,a9 by ANALMETR:40;
then  LIN o9,a9,b9 by AFF_1:6;
then  LIN o,a,b by ANALMETR:40;
hence  contradiction by A99, ANALMETR:def_10; ::_thesis: verum
end;
then A105: a1 = b1 by A103, A104, ANALMETR:63;
A106: a1,c1 _|_ c,a1 by A95, A102, ANALMETR:61;
 a1,c1 _|_ c,a by A97, ANALMETR:61;
then A107: ( c,a1 // c,a or a1 = c1 ) by A106, ANALMETR:63;
 not c,a1 // c,a
proof
assume  c,a1 // c,a ; ::_thesis: contradiction
then  LIN c,o,a by A102, ANALMETR:def_10;
then  LIN c9,o9,a9 by ANALMETR:40;
then  LIN o9,c9,a9 by AFF_1:6;
then  LIN o,c,a by ANALMETR:40;
hence  contradiction by A98, ANALMETR:def_10; ::_thesis: verum
end;
hence  b,c _|_ b1,c1 by A105, A107, ANALMETR:39; ::_thesis: verum
end;
A108: now__::_thesis:_(_LIN_o,b,c_&_o_<>_a1_implies_b,c__|__b1,c1_)
assume that
A109: LIN o,b,c and
A110: o <> a1 ; ::_thesis: b,c _|_ b1,c1
A111: o <> b by A99, ANALMETR:39;
A112: o <> c
proof
assume  o = c ; ::_thesis: contradiction
then  o,a // o,c by ANALMETR:39;
then  o9,a9 // o9,c9 by ANALMETR:36;
then  o9,c9 // o9,a9 by AFF_1:4;
hence  contradiction by A98, ANALMETR:36; ::_thesis: verum
end;
A113: o <> b1
proof
assume A114: o = b1 ; ::_thesis: contradiction
 a1,o _|_ a,o by A93, ANALMETR:61;
then  a,o // a,b by A96, A110, A114, ANALMETR:63;
then  LIN a,o,b by ANALMETR:def_10;
then  LIN a9,o9,b9 by ANALMETR:40;
then  LIN o9,a9,b9 by AFF_1:6;
then  LIN o,a,b by ANALMETR:40;
hence  contradiction by A99, ANALMETR:def_10; ::_thesis: verum
end;
 o,b // o,c by A109, ANALMETR:def_10;
then  o,c _|_ o,b1 by A94, A111, ANALMETR:62;
then  o,b1 // o,c1 by A95, A112, ANALMETR:63;
then  LIN o,b1,c1 by ANALMETR:def_10;
then  LIN o9,b19,c19 by ANALMETR:40;
then  LIN b19,o9,c19 by AFF_1:6;
then  LIN b1,o,c1 by ANALMETR:40;
then A115: b1,o // b1,c1 by ANALMETR:def_10;
 b1,o _|_ b,o by A94, ANALMETR:61;
then A116: b,o _|_ b1,c1 by A113, A115, ANALMETR:62;
 LIN o9,b9,c9 by A109, ANALMETR:40;
then  LIN b9,o9,c9 by AFF_1:6;
then  LIN b,o,c by ANALMETR:40;
then  b,o // b,c by ANALMETR:def_10;
hence  b,c _|_ b1,c1 by A111, A116, ANALMETR:62; ::_thesis: verum
end;
A117: now__::_thesis:_(_LIN_a,b,c_&_not_LIN_o,b,c_&_o_<>_a1_implies_b,c__|__b1,c1_)
assume that
A118: LIN a,b,c and
 not LIN o,b,c and
A119: o <> a1 ; ::_thesis: b,c _|_ b1,c1
A120: a <> c
proof
assume  a = c ; ::_thesis: contradiction
then  a,o // a,c by ANALMETR:39;
then  LIN a,o,c by ANALMETR:def_10;
then  LIN a9,o9,c9 by ANALMETR:40;
then  LIN o9,c9,a9 by AFF_1:6;
then  LIN o,c,a by ANALMETR:40;
hence  contradiction by A98, ANALMETR:def_10; ::_thesis: verum
end;
A121: a <> b
proof
assume  a = b ; ::_thesis: contradiction
then  a,o // a,b by ANALMETR:39;
then  LIN a,o,b by ANALMETR:def_10;
then  LIN a9,o9,b9 by ANALMETR:40;
then  LIN o9,a9,b9 by AFF_1:6;
then  LIN o,a,b by ANALMETR:40;
hence  contradiction by A99, ANALMETR:def_10; ::_thesis: verum
end;
A122: a1 <> b1 by A93, A94, A99, A119, ANALMETR:63;
 a,b // a,c by A118, ANALMETR:def_10;
then  a,c _|_ a1,b1 by A96, A121, ANALMETR:62;
then  a1,b1 // a1,c1 by A97, A120, ANALMETR:63;
then  LIN a1,b1,c1 by ANALMETR:def_10;
then  LIN a19,b19,c19 by ANALMETR:40;
then  LIN b19,a19,c19 by AFF_1:6;
then  LIN b1,a1,c1 by ANALMETR:40;
then A123: b1,a1 // b1,c1 by ANALMETR:def_10;
 b1,a1 _|_ b,a by A96, ANALMETR:61;
then A124: b,a _|_ b1,c1 by A122, A123, ANALMETR:62;
 LIN a9,b9,c9 by A118, ANALMETR:40;
then  LIN b9,a9,c9 by AFF_1:6;
then  LIN b,a,c by ANALMETR:40;
then  b,a // b,c by ANALMETR:def_10;
hence  b,c _|_ b1,c1 by A121, A124, ANALMETR:62; ::_thesis: verum
end;
now__::_thesis:_(_not_LIN_a,b,c_&_not_LIN_o,b,c_&_o_<>_a1_implies_b,c__|__b1,c1_)
assume that
A125: not LIN a,b,c and
A126: not LIN o,b,c and
A127: o <> a1 ; ::_thesis: b,c _|_ b1,c1
A128: o <> a by A98, ANALMETR:39;
A129: o <> c
proof
assume  o = c ; ::_thesis: contradiction
then  o,a // o,c by ANALMETR:39;
then  o9,a9 // o9,c9 by ANALMETR:36;
then  o9,c9 // o9,a9 by AFF_1:4;
hence  contradiction by A98, ANALMETR:36; ::_thesis: verum
end;
A130: o <> b1
proof
assume A131: o = b1 ; ::_thesis: contradiction
 a1,o _|_ a,o by A93, ANALMETR:61;
then  a,o // a,b by A96, A127, A131, ANALMETR:63;
then  LIN a,o,b by ANALMETR:def_10;
then  LIN a9,o9,b9 by ANALMETR:40;
then  LIN o9,a9,b9 by AFF_1:6;
then  LIN o,a,b by ANALMETR:40;
hence  contradiction by A99, ANALMETR:def_10; ::_thesis: verum
end;
A132: o <> c1
proof
assume A133: o = c1 ; ::_thesis: contradiction
 a1,o _|_ a,o by A93, ANALMETR:61;
then  a,o // a,c by A97, A127, A133, ANALMETR:63;
then  LIN a,o,c by ANALMETR:def_10;
then  LIN a9,o9,c9 by ANALMETR:40;
then  LIN o9,c9,a9 by AFF_1:6;
then  LIN o,c,a by ANALMETR:40;
hence  contradiction by A98, ANALMETR:def_10; ::_thesis: verum
end;
A134: o <> a by A98, ANALMETR:39;
A135: o <> b by A99, ANALMETR:39;
A136: a <> a1 by A93, A128, ANALMETR:39;
 ex e being Element of X st
( LIN b,c,e & LIN o,e,a & c <> e & e <> b & a <> e )
proof
consider p being Element of X such that
A137: o,a // o,p and
A138: o <> p by ANALMETR:39;
reconsider p9 = p as Element of (Af X) by ANALMETR:35;
consider p1 being Element of X such that
A139: b,c // b,p1 and
A140: b <> p1 by ANALMETR:39;
reconsider p19 = p1 as Element of (Af X) by ANALMETR:35;
 not o,p // b,p1
proof
assume  o,p // b,p1 ; ::_thesis: contradiction
then  b,p1 // o,a by A137, A138, ANALMETR:60;
then  o,a // b,c by A139, A140, ANALMETR:60;
then  o9,a9 // b9,c9 by ANALMETR:36;
then  o9,a9 // c9,b9 by AFF_1:4;
hence  contradiction by A100, ANALMETR:36; ::_thesis: verum
end;
then  not o9,p9 // b9,p19 by ANALMETR:36;
then consider e9 being Element of (Af X) such that
A141: LIN o9,p9,e9 and
A142: LIN b9,p19,e9 by AFF_1:60;
reconsider e = e9 as Element of X by ANALMETR:35;
 LIN o,p,e by A141, ANALMETR:40;
then A143: o,p // o,e by ANALMETR:def_10;
then  o,e // o,a by A137, A138, ANALMETR:60;
then A144: LIN o,e,a by ANALMETR:def_10;
 LIN b,p1,e by A142, ANALMETR:40;
then  b,p1 // b,e by ANALMETR:def_10;
then  b,c // b,e by A139, A140, ANALMETR:60;
then A145: LIN b,c,e by ANALMETR:def_10;
A146: c <> e by A98, A137, A138, A143, ANALMETR:60;
A147: b <> e
proof
assume  b = e ; ::_thesis: contradiction
then  LIN o9,b9,a9 by A144, ANALMETR:40;
then  LIN o9,a9,b9 by AFF_1:6;
then  LIN o,a,b by ANALMETR:40;
hence  contradiction by A99, ANALMETR:def_10; ::_thesis: verum
end;
 a <> e
proof
assume  a = e ; ::_thesis: contradiction
then  LIN b9,c9,a9 by A145, ANALMETR:40;
then  LIN a9,b9,c9 by AFF_1:6;
hence  contradiction by A125, ANALMETR:40; ::_thesis: verum
end;
hence  ex e being Element of X st
( LIN b,c,e & LIN o,e,a & c <> e & e <> b & a <> e ) by A144, A145, A146, A147; ::_thesis: verum
end;
then consider e being Element of X such that
A148: LIN b,c,e and
A149: LIN o,e,a and
A150: e <> b and
A151: c <> e and
A152: a <> e ;
reconsider e9 = e as Element of (Af X) by ANALMETR:35;
 ex e1 being Element of X st
( LIN o,e1,a1 & e,e1 // a,a1 )
proof
consider p being Element of X such that
A153: o,a1 // o,p and
A154: o <> p by ANALMETR:39;
reconsider p9 = p as Element of (Af X) by ANALMETR:35;
consider p1 being Element of X such that
A155: a,a1 // e,p1 and
A156: e <> p1 by ANALMETR:39;
reconsider p19 = p1 as Element of (Af X) by ANALMETR:35;
 not o,p // e,p1
proof
assume  o,p // e,p1 ; ::_thesis: contradiction
then  e,p1 // o,a1 by A153, A154, ANALMETR:60;
then  e9,p19 // o9,a19 by ANALMETR:36;
then  o9,a19 // e9,p19 by AFF_1:4;
then  o,a1 // e,p1 by ANALMETR:36;
then  e,p1 _|_ o,a by A93, A127, ANALMETR:62;
then  o,a _|_ a,a1 by A155, A156, ANALMETR:62;
then A157: o,a _|_ a1,a by ANALMETR:61;
 o,a _|_ a1,o by A93, ANALMETR:61;
then  a1,o // a1,a by A134, A157, ANALMETR:63;
then  LIN a1,o,a by ANALMETR:def_10;
then  LIN a19,o9,a9 by ANALMETR:40;
then  LIN a9,o9,a19 by AFF_1:6;
then  a9,o9 // a9,a19 by AFF_1:def_1;
then  o9,a9 // a19,a9 by AFF_1:4;
then  o,a // a1,a by ANALMETR:36;
then  a1,a _|_ a1,a by A134, A157, ANALMETR:62;
hence  contradiction by A136, ANALMETR:39; ::_thesis: verum
end;
then  not o9,p9 // e9,p19 by ANALMETR:36;
then consider e19 being Element of (Af X) such that
A158: LIN o9,p9,e19 and
A159: LIN e9,p19,e19 by AFF_1:60;
reconsider e1 = e19 as Element of X by ANALMETR:35;
 LIN o,p,e1 by A158, ANALMETR:40;
then  o,p // o,e1 by ANALMETR:def_10;
then  o,e1 // o,a1 by A153, A154, ANALMETR:60;
then A160: LIN o,e1,a1 by ANALMETR:def_10;
 LIN e,p1,e1 by A159, ANALMETR:40;
then  e,p1 // e,e1 by ANALMETR:def_10;
then  e,e1 // a,a1 by A155, A156, ANALMETR:60;
hence  ex e1 being Element of X st
( LIN o,e1,a1 & e,e1 // a,a1 ) by A160; ::_thesis: verum
end;
then consider e1 being Element of X such that
A161: LIN o,e1,a1 and
A162: e,e1 // a,a1 ;
reconsider e19 = e1 as Element of (Af X) by ANALMETR:35;
 o,e // o,a by A149, ANALMETR:def_10;
then  o9,e9 // o9,a9 by ANALMETR:36;
then  o9,a9 // o9,e9 by AFF_1:4;
then  o,a // o,e by ANALMETR:36;
then A163: o,a1 _|_ o,e by A93, A134, ANALMETR:62;
 o,e1 // o,a1 by A161, ANALMETR:def_10;
then  o9,e19 // o9,a19 by ANALMETR:36;
then  o9,a19 // o9,e19 by AFF_1:4;
then A164: o,a1 // o,e1 by ANALMETR:36;
A165: o <> e
proof
assume  o = e ; ::_thesis: contradiction
then  LIN b9,c9,o9 by A148, ANALMETR:40;
then  LIN o9,b9,c9 by AFF_1:6;
hence  contradiction by A126, ANALMETR:40; ::_thesis: verum
end;
A166: o <> e1
proof
assume  o = e1 ; ::_thesis: contradiction
then  e9,o9 // a9,a19 by A162, ANALMETR:36;
then  o9,e9 // a9,a19 by AFF_1:4;
then A167: o,e // a,a1 by ANALMETR:36;
 o,e // o,a by A149, ANALMETR:def_10;
then A168: o,a // a,a1 by A165, A167, ANALMETR:60;
then A169: o,a1 _|_ a,a1 by A93, A134, ANALMETR:62;
 o9,a9 // a9,a19 by A168, ANALMETR:36;
then  a9,o9 // a9,a19 by AFF_1:4;
then  LIN a9,o9,a19 by AFF_1:def_1;
then  LIN a19,o9,a9 by AFF_1:6;
then  a19,o9 // a19,a9 by AFF_1:def_1;
then  o9,a19 // a9,a19 by AFF_1:4;
then  o,a1 // a,a1 by ANALMETR:36;
then  a,a1 _|_ a,a1 by A127, A169, ANALMETR:62;
hence  contradiction by A136, ANALMETR:39; ::_thesis: verum
end;
A170: o,e _|_ o,e1 by A127, A163, A164, ANALMETR:62;
A171: not LIN o,b,a
proof
assume  LIN o,b,a ; ::_thesis: contradiction
then  o,b // o,a by ANALMETR:def_10;
then  o9,b9 // o9,a9 by ANALMETR:36;
then  o9,a9 // o9,b9 by AFF_1:4;
hence  contradiction by A99, ANALMETR:36; ::_thesis: verum
end;
 o,e // o,a by A149, ANALMETR:def_10;
then  o9,e9 // o9,a9 by ANALMETR:36;
then  o9,a9 // o9,e9 by AFF_1:4;
then  o,a // o,e by ANALMETR:36;
then A172: LIN o,a,e by ANALMETR:def_10;
 o,e1 // o,a1 by A161, ANALMETR:def_10;
then  o9,e19 // o9,a19 by ANALMETR:36;
then  o9,a19 // o9,e19 by AFF_1:4;
then  o,a1 // o,e1 by ANALMETR:36;
then A173: LIN o,a1,e1 by ANALMETR:def_10;
 e9,e19 // a9,a19 by A162, ANALMETR:36;
then  a9,a19 // e9,e19 by AFF_1:4;
then A174: a,a1 // e,e1 by ANALMETR:36;
then A175: e,b _|_ e1,b1 by A9, A93, A94, A96, A127, A130, A134, A135, A152, A165, A166, A170, A171, A172, A173, Def6;
 not LIN o,c,a by A98, ANALMETR:def_10;
then A176: e,c _|_ e1,c1 by A9, A93, A95, A97, A127, A129, A132, A134, A152, A165, A166, A170, A172, A173, A174, Def6;
A177: e1 <> b1
proof
assume  e1 = b1 ; ::_thesis: contradiction
then  o,b1 // o,a1 by A161, ANALMETR:def_10;
then  o,a1 _|_ o,b by A94, A130, ANALMETR:62;
hence  contradiction by A93, A99, A127, ANALMETR:63; ::_thesis: verum
end;
A178: c,e _|_ c1,e1 by A176, ANALMETR:61;
A179: LIN b9,c9,e9 by A148, ANALMETR:40;
then  LIN c9,e9,b9 by AFF_1:6;
then  LIN c,e,b by ANALMETR:40;
then  c,e // c,b by ANALMETR:def_10;
then A180: c,b _|_ c1,e1 by A151, A178, ANALMETR:62;
A181: c <> b
proof
assume  c = b ; ::_thesis: contradiction
then  LIN o9,b9,c9 by AFF_1:7;
hence  contradiction by A126, ANALMETR:40; ::_thesis: verum
end;
 b9,c9 // b9,e9 by A179, AFF_1:def_1;
then  c9,b9 // e9,b9 by AFF_1:4;
then  c,b // e,b by ANALMETR:36;
then  e,b _|_ c1,e1 by A180, A181, ANALMETR:62;
then  e1,b1 // c1,e1 by A150, A175, ANALMETR:63;
then  e19,b19 // c19,e19 by ANALMETR:36;
then  e19,b19 // e19,c19 by AFF_1:4;
then  LIN e19,b19,c19 by AFF_1:def_1;
then  LIN b19,e19,c19 by AFF_1:6;
then  b19,e19 // b19,c19 by AFF_1:def_1;
then  e19,b19 // b19,c19 by AFF_1:4;
then A182: e1,b1 // b1,c1 by ANALMETR:36;
 LIN b9,e9,c9 by A179, AFF_1:6;
then  b9,e9 // b9,c9 by AFF_1:def_1;
then  e9,b9 // b9,c9 by AFF_1:4;
then  e,b // b,c by ANALMETR:36;
then  e1,b1 _|_ b,c by A150, A175, ANALMETR:62;
hence  b,c _|_ b1,c1 by A177, A182, ANALMETR:62; ::_thesis: verum
end;
hence  b,c _|_ b1,c1 by A101, A108, A117; ::_thesis: verum
end;
then A183: ( not o,a // c,b implies b,c _|_ b1,c1 ) by A2, A3, A4, A5, A6, A7, A8;
now__::_thesis:_for_o,_a,_a1,_b,_b1,_c,_c1_being_Element_of_X_st_X_is_satisfying_LIN_&_o,a__|__o,a1_&_o,b__|__o,b1_&_o,c__|__o,c1_&_a,b__|__a1,b1_&_a,c__|__a1,c1_&_not_o,c_//_o,a_&_not_o,a_//_o,b_&_o,a_//_c,b_&_o,b_//_a,c_holds_
b,c__|__b1,c1
let o, a, a1, b, b1, c, c1 be Element of X; ::_thesis: ( X is satisfying_LIN & o,a _|_ o,a1 & o,b _|_ o,b1 & o,c _|_ o,c1 & a,b _|_ a1,b1 & a,c _|_ a1,c1 & not o,c // o,a & not o,a // o,b & o,a // c,b & o,b // a,c implies b,c _|_ b1,c1 )
assume  X is satisfying_LIN ; ::_thesis: ( o,a _|_ o,a1 & o,b _|_ o,b1 & o,c _|_ o,c1 & a,b _|_ a1,b1 & a,c _|_ a1,c1 & not o,c // o,a & not o,a // o,b & o,a // c,b & o,b // a,c implies b,c _|_ b1,c1 )
assume that
A184: o,a _|_ o,a1 and
A185: o,b _|_ o,b1 and
A186: o,c _|_ o,c1 and
A187: a,b _|_ a1,b1 and
A188: a,c _|_ a1,c1 and
A189: not o,c // o,a and
A190: not o,a // o,b ; ::_thesis: ( o,a // c,b & o,b // a,c implies b,c _|_ b1,c1 )
assume that
A191: o,a // c,b and
 o,b // a,c ; ::_thesis: b,c _|_ b1,c1
reconsider a9 = a, b9 = b, c9 = c, o9 = o as Element of (Af X) by ANALMETR:35;
A192: now__::_thesis:_(_o_=_a1_implies_b,c__|__b1,c1_)
assume A193: o = a1 ; ::_thesis: b,c _|_ b1,c1
then A194: a1,b1 _|_ b,a1 by A185, ANALMETR:61;
A195: a1,b1 _|_ b,a by A187, ANALMETR:61;
 not b,a1 // b,a
proof
assume  b,a1 // b,a ; ::_thesis: contradiction
then  LIN b,o,a by A193, ANALMETR:def_10;
then  LIN b9,o9,a9 by ANALMETR:40;
then  LIN o9,a9,b9 by AFF_1:6;
then  LIN o,a,b by ANALMETR:40;
hence  contradiction by A190, ANALMETR:def_10; ::_thesis: verum
end;
then A196: a1 = b1 by A194, A195, ANALMETR:63;
A197: a1,c1 _|_ c,a1 by A186, A193, ANALMETR:61;
 a1,c1 _|_ c,a by A188, ANALMETR:61;
then A198: ( c,a1 // c,a or a1 = c1 ) by A197, ANALMETR:63;
 not c,a1 // c,a
proof
assume  c,a1 // c,a ; ::_thesis: contradiction
then  LIN c,o,a by A193, ANALMETR:def_10;
then  LIN c9,o9,a9 by ANALMETR:40;
then  LIN o9,c9,a9 by AFF_1:6;
then  LIN o,c,a by ANALMETR:40;
hence  contradiction by A189, ANALMETR:def_10; ::_thesis: verum
end;
hence  b,c _|_ b1,c1 by A196, A198, ANALMETR:39; ::_thesis: verum
end;
A199: now__::_thesis:_(_o,a1_//_c1,b1_&_o_<>_a1_implies_b,c__|__b1,c1_)
assume that
A200: o,a1 // c1,b1 and
A201: o <> a1 ; ::_thesis: b,c _|_ b1,c1
 o <> a
proof
assume  o = a ; ::_thesis: contradiction
then  LIN o9,c9,a9 by AFF_1:7;
then  LIN o,c,a by ANALMETR:40;
hence  contradiction by A189, ANALMETR:def_10; ::_thesis: verum
end;
then  c,b _|_ o,a1 by A184, A191, ANALMETR:62;
then  c,b _|_ c1,b1 by A200, A201, ANALMETR:62;
hence  b,c _|_ b1,c1 by ANALMETR:61; ::_thesis: verum
end;
now__::_thesis:_(_not_o,a1_//_c1,b1_&_o_<>_a1_implies_b,c__|__b1,c1_)
assume that
A202: not o,a1 // c1,b1 and
A203: o <> a1 ; ::_thesis: b,c _|_ b1,c1
A204: o,a1 _|_ o,a by A184, ANALMETR:61;
A205: o,b1 _|_ o,b by A185, ANALMETR:61;
A206: o,c1 _|_ o,c by A186, ANALMETR:61;
A207: a1,b1 _|_ a,b by A187, ANALMETR:61;
A208: a1,c1 _|_ a,c by A188, ANALMETR:61;
A209: not o,c1 // o,a1
proof
assume A210: o,c1 // o,a1 ; ::_thesis: contradiction
 o <> c1
proof
assume  o = c1 ; ::_thesis: contradiction
then  a,c _|_ o,a1 by A188, ANALMETR:61;
then  a,c // o,a by A184, A203, ANALMETR:63;
then  a,c // a,o by ANALMETR:59;
then  LIN a,c,o by ANALMETR:def_10;
then  LIN a9,c9,o9 by ANALMETR:40;
then  LIN o9,c9,a9 by AFF_1:6;
then  LIN o,c,a by ANALMETR:40;
hence  contradiction by A189, ANALMETR:def_10; ::_thesis: verum
end;
then  o,c _|_ o,a1 by A186, A210, ANALMETR:62;
hence  contradiction by A184, A189, A203, ANALMETR:63; ::_thesis: verum
end;
 not o,a1 // o,b1
proof
assume A211: o,a1 // o,b1 ; ::_thesis: contradiction
A212: o <> b1
proof
assume  o = b1 ; ::_thesis: contradiction
then  a,b _|_ o,a1 by A187, ANALMETR:61;
then  a,b // o,a by A184, A203, ANALMETR:63;
then  a,b // a,o by ANALMETR:59;
then  LIN a,b,o by ANALMETR:def_10;
then  LIN a9,b9,o9 by ANALMETR:40;
then  LIN o9,a9,b9 by AFF_1:6;
then  LIN o,a,b by ANALMETR:40;
hence  contradiction by A190, ANALMETR:def_10; ::_thesis: verum
end;
 o,a _|_ o,b1 by A184, A203, A211, ANALMETR:62;
hence  contradiction by A185, A190, A212, ANALMETR:63; ::_thesis: verum
end;
then  b1,c1 _|_ b,c by A92, A202, A204, A205, A206, A207, A208, A209;
hence  b,c _|_ b1,c1 by ANALMETR:61; ::_thesis: verum
end;
hence  b,c _|_ b1,c1 by A192, A199; ::_thesis: verum
end;
hence  b,c _|_ b1,c1 by A1, A2, A3, A4, A5, A6, A7, A8, A91, A183; ::_thesis: verum
end;

theorem :: CONAFFM:6
for X being OrtAfPl st X is satisfying_LIN holds
X is satisfying_3H
proof
let X be OrtAfPl; ::_thesis: ( X is satisfying_LIN implies X is satisfying_3H )
assume A1: X is satisfying_LIN ; ::_thesis: X is satisfying_3H
let a be Element of X; :: according to CONAFFM:def_3 ::_thesis: 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; ::_thesis: ( 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 ; ::_thesis: 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 (Af X) by ANALMETR:35;
 not a9,e19 // b9,e29
proof
assume  a9,e19 // b9,e29 ; ::_thesis: 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; ::_thesis: verum
end;
then consider d9 being Element of (Af 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 by ANALMETR:35;
take  d ; ::_thesis: ( 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__::_thesis:_(_d_<>_c_implies_(_d,a__|__b,c_&_d,b__|__a,c_&_d,c__|__a,b_)_)
assume A17: d <> c ; ::_thesis: ( d,a _|_ b,c & d,b _|_ a,c & d,c _|_ a,b )
now__::_thesis:_(_b_<>_d_implies_(_d,a__|__b,c_&_d,b__|__a,c_&_d,c__|__a,b_)_)
assume A18: b <> d ; ::_thesis: ( d,a _|_ b,c & d,b _|_ a,c & d,c _|_ a,b )
 not b9,d9 // a9,c9
proof
assume  b9,d9 // a9,c9 ; ::_thesis: contradiction
then  a9,c9 // b9,d9 by AFF_1:4;
then A19: a,c // b,d by ANALMETR:36;
 a <> c
proof
assume  a = c ; ::_thesis: contradiction
then  LIN a9,b9,c9 by AFF_1:7;
hence  contradiction by A2, ANALMETR:40; ::_thesis: verum
end;
then  b,d _|_ b,d by A10, A19, ANALMETR:62;
hence  contradiction by A18, ANALMETR:39; ::_thesis: verum
end;
then consider o9 being Element of (Af 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 by ANALMETR:35;
now__::_thesis:_(_d_<>_a_implies_(_d,a__|__b,c_&_d,b__|__a,c_&_d,c__|__a,b_)_)
assume A22: d <> a ; ::_thesis: ( d,a _|_ b,c & d,b _|_ a,c & d,c _|_ a,b )
A23: o <> a
proof
assume A24: o = a ; ::_thesis: 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
proof
assume  a = b ; ::_thesis: contradiction
then  LIN a9,b9,c9 by AFF_1:7;
hence  contradiction by A2, ANALMETR:40; ::_thesis: verum
end;
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; ::_thesis: verum
end;
A27: c <> o
proof
assume A28: c = o ; ::_thesis: 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
proof
assume  b = c ; ::_thesis: contradiction
then  LIN a9,b9,c9 by AFF_1:7;
hence  contradiction by A2, ANALMETR:40; ::_thesis: verum
end;
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; ::_thesis: 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 (Af X) by ANALMETR:35;
 not a9,e19 // d9,e29
proof
assume  a9,e19 // d9,e29 ; ::_thesis: 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; ::_thesis: verum
end;
then consider d19 being Element of (Af 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 by ANALMETR:35;
 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 ; ::_thesis: 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
proof
assume  a = c ; ::_thesis: contradiction
then  LIN a9,b9,c9 by AFF_1:7;
hence  contradiction by A2, ANALMETR:40; ::_thesis: verum
end;
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; ::_thesis: verum
end;
A45: o <> d1
proof
assume A46: o = d1 ; ::_thesis: 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; ::_thesis: verum
end;
A48: o <> b
proof
assume  o = b ; ::_thesis: contradiction
then  LIN a9,b9,c9 by A21, AFF_1:6;
hence  contradiction by A2, ANALMETR:40; ::_thesis: verum
end;
A49: d1 <> c
proof
assume A50: d1 = c ; ::_thesis: contradiction
A51: b <> c
proof
assume  b = c ; ::_thesis: contradiction
then  LIN a9,b9,c9 by AFF_1:7;
hence  contradiction by A2, ANALMETR:40; ::_thesis: verum
end;
 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; ::_thesis: 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
proof
assume  a = c ; ::_thesis: contradiction
then  LIN a9,b9,c9 by AFF_1:7;
hence  contradiction by A2, ANALMETR:40; ::_thesis: verum
end;
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
proof
assume  a = c ; ::_thesis: contradiction
then  LIN a9,b9,c9 by AFF_1:7;
hence  contradiction by A2, ANALMETR:40; ::_thesis: verum
end;
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
proof
assume  a = c ; ::_thesis: contradiction
then  LIN a9,b9,c9 by AFF_1:7;
hence  contradiction by A2, ANALMETR:40; ::_thesis: verum
end;
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
proof
assume  LIN o,d,d1 ; ::_thesis: contradiction
then  o,d // o,d1 by ANALMETR:def_10;
then  o,d _|_ o,d by A45, A62, ANALMETR:62;
hence  contradiction by A40, ANALMETR:39; ::_thesis: verum
end;
 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
proof
assume  a = c ; ::_thesis: contradiction
then  LIN a9,b9,c9 by AFF_1:7;
hence  contradiction by A2, ANALMETR:40; ::_thesis: verum
end;
 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
proof
assume  b = c ; ::_thesis: contradiction
then  LIN a9,b9,c9 by AFF_1:7;
hence  contradiction by A2, ANALMETR:40; ::_thesis: verum
end;
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, Def6;
hence  ( d,a _|_ b,c & d,b _|_ a,c & d,c _|_ a,b ) by A10, A13, ANALMETR:61; ::_thesis: verum
end;
hence  ( d,a _|_ b,c & d,b _|_ a,c & d,c _|_ a,b ) by A3, A4, A10, A12, ANALMETR:61, ANALMETR:62; ::_thesis: verum
end;
hence  ( d,a _|_ b,c & d,b _|_ a,c & d,c _|_ a,b ) by A5, A6, A9, A13, ANALMETR:61, ANALMETR:62; ::_thesis: verum
end;
now__::_thesis:_(_d_=_c_implies_(_d,a__|__b,c_&_d,b__|__a,c_&_d,c__|__a,b_)_)
assume  d = c ; ::_thesis: ( 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; ::_thesis: verum
end;
hence  ( d,a _|_ b,c & d,b _|_ a,c & d,c _|_ a,b ) by A16; ::_thesis: verum
end;