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 & a <> e1 ) by ANALMETR:def 10;
consider e2 being Element of X such that
A4: ( a,c _|_ b,e2 & b <> e2 ) by ANALMETR:def 10;
reconsider a' = a, b' = b, c' = c, e1' = e1, e2' = e2 as Element of (Af X) by ANALMETR:47;
not a',e1' // b',e2'

proof

assume a',e1' // b',e2' ; :: thesis: contradiction
then a,e1 // b,e2 by ANALMETR:48;
then b,e2 _|_ b,c by A3, ANALMETR:84;
then a,c // b,c by A4, ANALMETR:85;
then a',c' // b',c' by ANALMETR:48;
then c',a' // c',b' by AFF_1:13;
then LIN c',a',b' by AFF_1:def 1;
then LIN a',b',c' by AFF_1:15;
hence contradiction by A2, ANALMETR:55; :: thesis: verum

end;

then consider d' being Element of (Af X) such that
A5: ( LIN a',e1',d' & LIN b',e2',d' ) by AFF_1:74;
reconsider d = d' as Element of X by ANALMETR:47;
take d ; :: thesis: ( d,a _|_ b,c & d,b _|_ a,c & d,c _|_ a,b )
LIN b,e2,d by A5, ANALMETR:55;
then A6: b,e2 // b,d by ANALMETR:def 11;
then A7: a,c _|_ b,d by A4, ANALMETR:84;
then A8: d,b _|_ a,c by ANALMETR:83;
LIN a,e1,d by A5, ANALMETR:55;
then A9: a,e1 // a,d by ANALMETR:def 11;
then A10: b,c _|_ a,d by A3, ANALMETR:84;
then A11: d,a _|_ b,c by ANALMETR:83;
A12: X is satisfying_LIN1 by A1, Th3;

A13: now

assume A14: d <> c ; :: thesis: ( d,a _|_ b,c & d,b _|_ a,c & d,c _|_ a,b )

now

assume A15: b <> d ; :: thesis: ( d,a _|_ b,c & d,b _|_ a,c & d,c _|_ a,b )
not b',d' // a',c'

proof

assume b',d' // a',c' ; :: thesis: contradiction
then a',c' // b',d' by AFF_1:13;
then A16: a,c // b,d by ANALMETR:48;
a <> c

proof

assume a = c ; :: thesis: contradiction
then LIN a',b',c' by AFF_1:16;
hence contradiction by A2, ANALMETR:55; :: thesis: verum

end;

then b,d _|_ b,d by A7, A16, ANALMETR:84;
hence contradiction by A15, ANALMETR:51; :: thesis: verum

end;

then consider o' being Element of (Af X) such that
A17: ( LIN b',d',o' & LIN a',c',o' ) by AFF_1:74;
reconsider o = o' as Element of X by ANALMETR:47;

now

assume A18: d <> a ; :: thesis: ( d,a _|_ b,c & d,b _|_ a,c & d,c _|_ a,b )
A19: o <> a

proof

assume A20: o = a ; :: thesis: contradiction
then LIN b,d,a by A17, ANALMETR:55;
then b,d // b,a by ANALMETR:def 11;
then b,a _|_ a,c by A7, A15, ANALMETR:84;
then A21: a,b _|_ a,c by ANALMETR:83;
LIN a',b',d' by A17, A20, AFF_1:15;
then LIN a,b,d by ANALMETR:55;
then A22: a,b // a,d by ANALMETR:def 11;
a <> b

proof

assume a = b ; :: thesis: contradiction
then LIN a',b',c' by AFF_1:16;
hence contradiction by A2, ANALMETR:55; :: thesis: verum

end;

then a,d _|_ a,c by A21, A22, ANALMETR:84;
then d,a _|_ a,c by ANALMETR:83;
then a,c // b,c by A11, A18, ANALMETR:85;
then c,a // c,b by ANALMETR:81;
then LIN c,a,b by ANALMETR:def 11;
then LIN c',a',b' by ANALMETR:55;
then LIN a',b',c' by AFF_1:15;
hence contradiction by A2, ANALMETR:55; :: thesis: verum

end;

A23: c <> o

proof

assume A24: c = o ; :: thesis: contradiction
then LIN b,d,c by A17, ANALMETR:55;
then b,d // b,c by ANALMETR:def 11;
then A25: b,c _|_ a,c by A7, A15, ANALMETR:84;
b <> c

proof

assume b = c ; :: thesis: contradiction
then LIN a',b',c' by AFF_1:16;
hence contradiction by A2, ANALMETR:55; :: thesis: verum

end;

then a,d // a,c by A10, A25, ANALMETR:85;
then LIN a,d,c by ANALMETR:def 11;
then LIN a',d',c' by ANALMETR:55;
then LIN c',d',a' by AFF_1:15;
then LIN c,d,a by ANALMETR:55;
then A26: c,d // c,a by ANALMETR:def 11;
LIN c',d',b' by A17, A24, AFF_1:15;
then LIN c,d,b by ANALMETR:55;
then c,d // c,b by ANALMETR:def 11;
then c,a // c,b by A14, A26, ANALMETR:82;
then LIN c,a,b by ANALMETR:def 11;
then LIN c',a',b' by ANALMETR:55;
then LIN a',b',c' by AFF_1:15;
hence contradiction by A2, ANALMETR:55; :: thesis: verum

end;

consider e1 being Element of X such that
A27: ( a,c // a,e1 & a <> e1 ) by ANALMETR:51;
consider e2 being Element of X such that
A28: ( b,c // d,e2 & d <> e2 ) by ANALMETR:51;
reconsider e1' = e1, e2' = e2 as Element of (Af X) by ANALMETR:47;
not a',e1' // d',e2'

proof

assume a',e1' // d',e2' ; :: thesis: contradiction
then a,e1 // d,e2 by ANALMETR:48;
then d,e2 // a,c by A27, ANALMETR:82;
then a,c // b,c by A28, ANALMETR:82;
then c,a // c,b by ANALMETR:81;
then LIN c,a,b by ANALMETR:def 11;
then LIN c',a',b' by ANALMETR:55;
then LIN a',b',c' by AFF_1:15;
hence contradiction by A2, ANALMETR:55; :: thesis: verum

end;

then consider d1' being Element of (Af X) such that
A29: ( LIN a',e1',d1' & LIN d',e2',d1' ) by AFF_1:74;
reconsider d1 = d1' as Element of X by ANALMETR:47;
A30: LIN a,c,d1

proof

LIN a,e1,d1 by A29, ANALMETR:55;
then a,e1 // a,d1 by ANALMETR:def 11;
then a,c // a,d1 by A27, ANALMETR:82;
hence LIN a,c,d1 by ANALMETR:def 11; :: thesis: verum

end;

A31: b,c // d,d1

proof

LIN d,e2,d1 by A29, ANALMETR:55;
then d,e2 // d,d1 by ANALMETR:def 11;
hence b,c // d,d1 by A28, ANALMETR:82; :: thesis: verum

end;

A32: o <> d

proof

assume A33: o = d ; :: thesis: contradiction
then A34: a,o _|_ b,c by A3, A9, ANALMETR:84;
LIN a,c,o by A17, ANALMETR:55;
then a,c // a,o by ANALMETR:def 11;
then A35: a,c _|_ b,c by A19, A34, ANALMETR:84;
a <> c

proof

assume a = c ; :: thesis: contradiction
then LIN a',b',c' by AFF_1:16;
hence contradiction by A2, ANALMETR:55; :: thesis: verum

end;

then b,o // b,c by A7, A33, A35, ANALMETR:85;
then LIN b,o,c by ANALMETR:def 11;
then LIN b',o',c' by ANALMETR:55;
then LIN c',o',b' by AFF_1:15;
then LIN c,o,b by ANALMETR:55;
then A36: c,o // c,b by ANALMETR:def 11;
LIN c',o',a' by A17, AFF_1:15;
then LIN c,o,a by ANALMETR:55;
then c,o // c,a by ANALMETR:def 11;
then c,b // c,a by A23, A36, ANALMETR:82;
then LIN c,b,a by ANALMETR:def 11;
then LIN c',b',a' by ANALMETR:55;
then LIN a',b',c' by AFF_1:15;
hence contradiction by A2, ANALMETR:55; :: thesis: verum

end;

A37: o <> d1

proof

assume A38: o = d1 ; :: thesis: contradiction
LIN o',d',b' by A17, AFF_1:15;
then LIN o,d,b by ANALMETR:55;
then o,d // o,b by ANALMETR:def 11;
then d,o // b,o by ANALMETR:81;
then b,c // b,o by A31, A32, A38, ANALMETR:82;
then LIN b,c,o by ANALMETR:def 11;
then LIN b',c',o' by ANALMETR:55;
then LIN c',o',b' by AFF_1:15;
then LIN c,o,b by ANALMETR:55;
then A39: c,o // c,b by ANALMETR:def 11;
LIN c',o',a' by A17, AFF_1:15;
then LIN c,o,a by ANALMETR:55;
then c,o // c,a by ANALMETR:def 11;
then c,a // c,b by A23, A39, ANALMETR:82;
then LIN c,a,b by ANALMETR:def 11;
then LIN c',a',b' by ANALMETR:55;
then LIN a',b',c' by AFF_1:15;
hence contradiction by A2, ANALMETR:55; :: thesis: verum

end;

A40: o <> b

proof

assume o = b ; :: thesis: contradiction
then LIN a',b',c' by A17, AFF_1:15;
hence contradiction by A2, ANALMETR:55; :: thesis: verum

end;

A41: d1 <> c

proof

assume A42: d1 = c ; :: thesis: contradiction
A43: b <> c

proof

assume b = c ; :: thesis: contradiction
then LIN a',b',c' by AFF_1:16;
hence contradiction by A2, ANALMETR:55; :: thesis: verum

end;

c,b // c,d by A31, A42, ANALMETR:81;
then LIN c,b,d by ANALMETR:def 11;
then A44: LIN c',b',d' by ANALMETR:55;
b,c // c,d by A31, A42, ANALMETR:81;
then d,a _|_ c,d by A11, A43, ANALMETR:84;
then A45: d,c _|_ d,a by ANALMETR:83;
LIN d',c',b' by A44, AFF_1:15;
then LIN d,c,b by ANALMETR:55;
then d,c // d,b by ANALMETR:def 11;
then d,b _|_ d,a by A14, A45, ANALMETR:84;
then a,c // d,a by A8, A15, ANALMETR:85;
then a,c // a,d by ANALMETR:81;
then LIN a,c,d by ANALMETR:def 11;
then LIN a',c',d' by ANALMETR:55;
then LIN c',a',d' by AFF_1:15;
then LIN c,a,d by ANALMETR:55;
then A46: c,a // c,d by ANALMETR:def 11;
c,d // b,c by A31, A42, ANALMETR:81;
then c,a // b,c by A14, A46, ANALMETR:82;
then c,a // c,b by ANALMETR:81;
then LIN c,a,b by ANALMETR:def 11;
then LIN c',a',b' by ANALMETR:55;
then LIN a',b',c' by AFF_1:15;
hence contradiction by A2, ANALMETR:55; :: thesis: verum

end;

A47: o,d _|_ o,a

proof

LIN d',o',b' by A17, AFF_1:15;
then d',o' // d',b' by AFF_1:def 1;
then b',d' // o',d' by AFF_1:13;
then b,d // o,d by ANALMETR:48;
then A48: a,c _|_ o,d by A7, A15, ANALMETR:84;
LIN a,c,o by A17, ANALMETR:55;
then a,c // a,o by ANALMETR:def 11;
then A49: a,c // o,a by ANALMETR:81;
a <> c

proof

assume a = c ; :: thesis: contradiction
then LIN a',b',c' by AFF_1:16;
hence contradiction by A2, ANALMETR:55; :: thesis: verum

end;

hence o,d _|_ o,a by A48, A49, ANALMETR:84; :: thesis: verum

end;

A50: o,d1 _|_ o,d

proof

LIN a,c,o by A17, ANALMETR:55;
then A51: a,c // a,o by ANALMETR:def 11;
A52: a <> c

proof

assume a = c ; :: thesis: contradiction
then LIN a',b',c' by AFF_1:16;
hence contradiction by A2, ANALMETR:55; :: thesis: verum

end;

a,c // a,d1 by A30, ANALMETR:def 11;
then a,o // a,d1 by A51, A52, ANALMETR:82;
then LIN a,o,d1 by ANALMETR:def 11;
then LIN a',o',d1' by ANALMETR:55;
then LIN o',a',d1' by AFF_1:15;
then LIN o,a,d1 by ANALMETR:55;
then A53: o,a // o,d1 by ANALMETR:def 11;
LIN a,c,o by A17, ANALMETR:55;
then a,c // a,o by ANALMETR:def 11;
then o,a // a,c by ANALMETR:81;
then a,c // o,d1 by A19, A53, ANALMETR:82;
then A54: b,d _|_ o,d1 by A7, A52, ANALMETR:84;
LIN d',o',b' by A17, AFF_1:15;
then LIN d,o,b by ANALMETR:55;
then d,o // d,b by ANALMETR:def 11;
then b,d // o,d by ANALMETR:81;
hence o,d1 _|_ o,d by A15, A54, ANALMETR:84; :: thesis: verum

end;

A55: o,c _|_ o,b

proof

LIN c',o',a' by A17, AFF_1:15;
then c',o' // c',a' by AFF_1:def 1;
then a',c' // o',c' by AFF_1:13;
then A56: a,c // o,c by ANALMETR:48;
a <> c

proof

assume a = c ; :: thesis: contradiction
then LIN a',b',c' by AFF_1:16;
hence contradiction by A2, ANALMETR:55; :: thesis: verum

end;

then A57: b,d _|_ o,c by A7, A56, ANALMETR:84;
b',d' // b',o' by A17, AFF_1:def 1;
then b',d' // o',b' by AFF_1:13;
then b,d // o,b by ANALMETR:48;
hence o,c _|_ o,b by A15, A57, ANALMETR:84; :: thesis: verum

end;

A58: not LIN o,d,d1

proof

assume LIN o,d,d1 ; :: thesis: contradiction
then o,d // o,d1 by ANALMETR:def 11;
then o,d _|_ o,d by A37, A50, ANALMETR:84;
hence contradiction by A32, ANALMETR:51; :: thesis: verum

end;

A59: LIN o,d1,c

proof

LIN a',c',d1' by A30, ANALMETR:55;
then LIN c',d1',a' by AFF_1:15;
then c',d1' // c',a' by AFF_1:def 1;
then a',c' // c',d1' by AFF_1:13;
then A60: a,c // c,d1 by ANALMETR:48;
A61: a <> c

proof

assume a = c ; :: thesis: contradiction
then LIN a',b',c' by AFF_1:16;
hence contradiction by A2, ANALMETR:55; :: thesis: verum

end;

LIN c',a',o' by A17, AFF_1:15;
then c',a' // c',o' by AFF_1:def 1;
then a',c' // c',o' by AFF_1:13;
then a,c // c,o by ANALMETR:48;
then c,d1 // c,o by A60, A61, ANALMETR:82;
then LIN c,d1,o by ANALMETR:def 11;
then LIN c',d1',o' by ANALMETR:55;
then LIN o',d1',c' by AFF_1:15;
hence LIN o,d1,c by ANALMETR:55; :: thesis: verum

end;

LIN o',d',b' by A17, AFF_1:15;
then A62: LIN o,d,b by ANALMETR:55;
A63: d1,d // c,b by A31, ANALMETR:81;
d1,d _|_ d,a

proof

b <> c

proof

assume b = c ; :: thesis: contradiction
then LIN a',b',c' by AFF_1:16;
hence contradiction by A2, ANALMETR:55; :: thesis: verum

end;

then d,d1 _|_ a,d by A10, A31, ANALMETR:84;
hence d1,d _|_ d,a by ANALMETR:83; :: thesis: verum

end;

then c,d _|_ b,a by A12, A19, A23, A32, A37, A40, A41, A47, A50, A55, A58, A59, A62, A63, Def6;
hence ( d,a _|_ b,c & d,b _|_ a,c & d,c _|_ a,b ) by A7, A10, ANALMETR:83; :: thesis: verum

end;

hence ( d,a _|_ b,c & d,b _|_ a,c & d,c _|_ a,b ) by A3, A7, A9, ANALMETR:83, ANALMETR:84; :: thesis: verum

end;

hence ( d,a _|_ b,c & d,b _|_ a,c & d,c _|_ a,b ) by A4, A6, A10, ANALMETR:83, ANALMETR:84; :: thesis: verum

end;

now

assume d = c ; :: thesis: ( d,a _|_ b,c & d,b _|_ a,c & d,c _|_ a,b )
then a,b _|_ d,c by ANALMETR:51;
hence ( d,a _|_ b,c & d,b _|_ a,c & d,c _|_ a,b ) by A7, A10, ANALMETR:83; :: thesis: verum

end;

hence ( d,a _|_ b,c & d,b _|_ a,c & d,c _|_ a,b ) by A13; :: thesis: verum