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 AffinStruct(# the U1 of X, the CONGR of X #) ;
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 A31: o <> b1 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 A39: a <> b 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 A47: o <> b1 A49: o <> c1 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 AffinStruct(# the U1 of X, the CONGR of X #) ;
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 AffinStruct(# the U1 of X, the CONGR of X #) ;
not o,p // a,p1 then not o9,p9 // a9,p19 by ANALMETR:36;
then consider e9 being Element of AffinStruct(# the U1 of X, the CONGR of 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 ;
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 AffinStruct(# the U1 of X, the CONGR of X #) ;
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 AffinStruct(# the U1 of X, the CONGR of X #) ;
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 AffinStruct(# the U1 of X, the CONGR of X #) ;
A72: not o,b1 // a1,c1 not o,p // a1,p1 then not o9,p9 // a19,p19 by ANALMETR:36;
then consider e19 being Element of AffinStruct(# the U1 of X, the CONGR of 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 ;
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 AffinStruct(# the U1 of X, the CONGR of X #) ;
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 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;
A88: not LIN o,c,e 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; :: 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 AffinStruct(# the U1 of X, the CONGR of X #) ;
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 A113: o <> b1 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 A121: a <> b 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 A130: o <> b1 A132: o <> c1 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 AffinStruct(# the U1 of X, the CONGR of X #) ;
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 AffinStruct(# the U1 of X, the CONGR of X #) ;
not o,p // b,p1 then not o9,p9 // b9,p19 by ANALMETR:36;
then consider e9 being Element of AffinStruct(# the U1 of X, the CONGR of 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 ;
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 AffinStruct(# the U1 of X, the CONGR of X #) ;
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 AffinStruct(# the U1 of X, the CONGR of X #) ;
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 AffinStruct(# the U1 of X, the CONGR of X #) ;
not o,p // e,p1 then not o9,p9 // e9,p19 by ANALMETR:36;
then consider e19 being Element of AffinStruct(# the U1 of X, the CONGR of 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 ;
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 AffinStruct(# the U1 of X, the CONGR of X #) ;
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 A170: o,e _|_ o,e1 by A127, A163, A164, ANALMETR:62;
A171: not LIN o,b,a 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;
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;
A177: e1 <> b1 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 AffinStruct(# the U1 of X, the CONGR of X #) ;
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 not o,a1 // o,b1 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