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 ; :: according to CONAFFM:def 3 :: thesis: for b, c being Element of st not LIN a,b,c holds
ex d being Element of st
( d,a _|_ b,c & d,b _|_ a,c & d,c _|_ a,b )
let b, c be Element of ; :: thesis: ( not LIN a,b,c implies ex d being Element of 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 st
( d,a _|_ b,c & d,b _|_ a,c & d,c _|_ a,b )
consider e1 being Element of such that
A3: b,c _|_ a,e1 and
A4: a <> e1 by ANALMETR:def 10;
consider e2 being Element of such that
A5: a,c _|_ b,e2 and
A6: b <> e2 by ANALMETR:def 10;
reconsider a' = a, b' = b, c' = c, e1' = e1, e2' = e2 as Element of 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, A4, ANALMETR:84;
then a,c // b,c by A5, A6, 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 such that
A7: LIN a',e1',d' and
A8: LIN b',e2',d' by AFF_1:74;
reconsider d = d' as Element of by ANALMETR:47;
take d ; :: thesis: ( d,a _|_ b,c & d,b _|_ a,c & d,c _|_ a,b )
LIN b,e2,d by A8, ANALMETR:55;
then A9: b,e2 // b,d by ANALMETR:def 11;
then A10: a,c _|_ b,d by A5, A6, ANALMETR:84;
then A11: d,b _|_ a,c by ANALMETR:83;
LIN a,e1,d by A7, ANALMETR:55;
then A12: a,e1 // a,d by ANALMETR:def 11;
then A13: b,c _|_ a,d by A3, A4, ANALMETR:84;
then A14: d,a _|_ b,c by ANALMETR:83;
A15: X is satisfying_LIN1 by A1, Th3;

A16: now

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

now

assume A18: 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 A19: 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 A10, A19, ANALMETR:84;
hence contradiction by A18, ANALMETR:51; :: thesis: verum

end;

then consider o' being Element of such that
A20: LIN b',d',o' and
A21: LIN a',c',o' by AFF_1:74;
reconsider o = o' as Element of by ANALMETR:47;

now

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:55;
then b,d // b,a by ANALMETR:def 11;
then b,a _|_ a,c by A10, A18, ANALMETR:84;
then A25: a,b _|_ a,c by ANALMETR:83;
LIN a',b',d' by A20, A24, AFF_1:15;
then LIN a,b,d by ANALMETR:55;
then A26: 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 A25, A26, ANALMETR:84;
then d,a _|_ a,c by ANALMETR:83;
then a,c // b,c by A14, A22, 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;

A27: c <> o

proof

assume A28: c = o ; :: thesis: contradiction
then LIN b,d,c by A20, ANALMETR:55;
then b,d // b,c by ANALMETR:def 11;
then A29: b,c _|_ a,c by A10, A18, 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 A13, A29, 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 A30: c,d // c,a by ANALMETR:def 11;
LIN c',d',b' by A20, A28, 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 A17, A30, 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 such that
A31: a,c // a,e1 and
A32: a <> e1 by ANALMETR:51;
consider e2 being Element of such that
A33: b,c // d,e2 and
A34: d <> e2 by ANALMETR:51;
reconsider e1' = e1, e2' = e2 as Element of 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 A31, A32, ANALMETR:82;
then a,c // b,c by A33, A34, 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 such that
A35: LIN a',e1',d1' and
A36: LIN d',e2',d1' by AFF_1:74;
reconsider d1 = d1' as Element of by ANALMETR:47;
LIN a,e1,d1 by A35, ANALMETR:55;
then a,e1 // a,d1 by ANALMETR:def 11;
then A37: a,c // a,d1 by A31, A32, ANALMETR:82;
then A38: LIN a,c,d1 by ANALMETR:def 11;
LIN d,e2,d1 by A36, ANALMETR:55;
then d,e2 // d,d1 by ANALMETR:def 11;
then A39: b,c // d,d1 by A33, A34, ANALMETR:82;
A40: o <> d

proof

assume A41: o = d ; :: thesis: contradiction
then A42: a,o _|_ b,c by A3, A4, A12, ANALMETR:84;
LIN a,c,o by A21, ANALMETR:55;
then a,c // a,o by ANALMETR:def 11;
then A43: a,c _|_ b,c by A23, A42, 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 A10, A41, A43, 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 A44: c,o // c,b by ANALMETR:def 11;
LIN c',o',a' by A21, 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 A27, A44, 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;

A45: o <> d1

proof

assume A46: o = d1 ; :: thesis: contradiction
LIN o',d',b' by A20, 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 A39, A40, A46, 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 A47: c,o // c,b by ANALMETR:def 11;
LIN c',o',a' by A21, 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 A27, A47, 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;

A48: o <> b

proof

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

end;

A49: d1 <> c

proof

assume A50: d1 = c ; :: thesis: contradiction
A51: 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 A39, A50, ANALMETR:81;
then LIN c,b,d by ANALMETR:def 11;
then A52: LIN c',b',d' by ANALMETR:55;
b,c // c,d by A39, A50, ANALMETR:81;
then d,a _|_ c,d by A14, A51, ANALMETR:84;
then A53: d,c _|_ d,a by ANALMETR:83;
LIN d',c',b' by A52, 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 A17, A53, ANALMETR:84;
then a,c // d,a by A11, A18, 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 A54: c,a // c,d by ANALMETR:def 11;
c,d // b,c by A39, A50, ANALMETR:81;
then c,a // b,c by A17, A54, 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;

LIN d',o',b' by A20, 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 A55: a,c _|_ o,d by A10, A18, ANALMETR:84;
LIN a,c,o by A21, ANALMETR:55;
then a,c // a,o by ANALMETR:def 11;
then A56: 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;

then A57: o,d _|_ o,a by A55, A56, ANALMETR:84;
LIN a,c,o by A21, ANALMETR:55;
then A58: a,c // a,o by ANALMETR:def 11;
A59: 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 a,o // a,d1 by A37, A58, 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 A60: o,a // o,d1 by ANALMETR:def 11;
LIN a,c,o by A21, 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 A23, A60, ANALMETR:82;
then A61: b,d _|_ o,d1 by A10, A59, ANALMETR:84;
LIN d',o',b' by A20, 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;
then A62: o,d1 _|_ o,d by A18, A61, ANALMETR:84;
LIN c',o',a' by A21, AFF_1:15;
then c',o' // c',a' by AFF_1:def 1;
then a',c' // o',c' by AFF_1:13;
then A63: 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 A64: b,d _|_ o,c by A10, A63, ANALMETR:84;
b',d' // b',o' by A20, AFF_1:def 1;
then b',d' // o',b' by AFF_1:13;
then b,d // o,b by ANALMETR:48;
then A65: o,c _|_ o,b by A18, A64, ANALMETR:84;
A66: 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 A45, A62, ANALMETR:84;
hence contradiction by A40, ANALMETR:51; :: thesis: verum

end;

LIN a',c',d1' by A38, 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 A67: a,c // c,d1 by ANALMETR:48;
A68: 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 A21, 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 A67, A68, 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;
then A69: LIN o,d1,c by ANALMETR:55;
LIN o',d',b' by A20, AFF_1:15;
then A70: LIN o,d,b by ANALMETR:55;
A71: d1,d // c,b by A39, ANALMETR:81;
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 A13, A39, ANALMETR:84;
then d1,d _|_ d,a by ANALMETR:83;
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:83; :: thesis: verum

end;

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

end;

hence ( d,a _|_ b,c & d,b _|_ a,c & d,c _|_ a,b ) by A5, A6, A9, A13, 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 A10, A13, ANALMETR:83; :: thesis: verum

end;

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