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 AffinStruct(# the U1 of X, the CONGR of X #) ;
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 AffinStruct(# the U1 of X, the CONGR of X #) ;
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 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 AffinStruct(# the U1 of X, the CONGR of 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 ;
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 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 AffinStruct(# the U1 of X, the CONGR of X #) ;
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;
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