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 AffinStruct(# the U1 of X, the CONGR of X #) ;
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 AffinStruct(# the U1 of X, the CONGR of 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 ;
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 then consider o9 being Element of AffinStruct(# the U1 of X, the CONGR of 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 ;
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 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 AffinStruct(# the U1 of X, the CONGR of X #) ;
not a9,e19 // d9,e29 then consider d19 being Element of AffinStruct(# the U1 of X, the CONGR of 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 ;
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 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 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;
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