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 A2: ( 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 ) ; :: thesis: b,c _|_ b1,c1
A3: X is satisfying_LIN1 by A1, Th3;
now
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 A4: 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 A5: ( 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 ) ; :: thesis: ( not o,b // a,c implies b,c _|_ b1,c1 )
assume A6: not o,b // a,c ; :: thesis: b,c _|_ b1,c1
reconsider a' = a, a1' = a1, b' = b, b1' = b1, c' = c, c1' = c1, o' = o as Element of (Af X) by ANALMETR:47;
A7: now
assume A8: o = a1 ; :: thesis: b,c _|_ b1,c1
then A9: a1,b1 _|_ b,a1 by A5, ANALMETR:83;
A10: a1,b1 _|_ b,a by A5, ANALMETR:83;
not b,a1 // b,a
proof
assume b,a1 // b,a ; :: thesis: contradiction
then LIN b,o,a by A8, ANALMETR:def 11;
then LIN b',o',a' by ANALMETR:55;
then LIN o',a',b' by AFF_1:15;
then LIN o,a,b by ANALMETR:55;
hence contradiction by A5, ANALMETR:def 11; :: thesis: verum
end;
then A11: a1 = b1 by A9, A10, ANALMETR:85;
A12: a1,c1 _|_ c,a1 by A5, A8, ANALMETR:83;
a1,c1 _|_ c,a by A5, ANALMETR:83;
then A13: ( c,a1 // c,a or a1 = c1 ) by A12, ANALMETR:85;
not c,a1 // c,a
proof
assume c,a1 // c,a ; :: thesis: contradiction
then LIN c,o,a by A8, ANALMETR:def 11;
then LIN c',o',a' by ANALMETR:55;
then LIN o',c',a' by AFF_1:15;
then LIN o,c,a by ANALMETR:55;
hence contradiction by A5, ANALMETR:def 11; :: thesis: verum
end;
hence b,c _|_ b1,c1 by A11, A13, ANALMETR:51; :: thesis: verum
end;
A14: now
assume A15: ( LIN o,b,c & o <> a1 ) ; :: thesis: b,c _|_ b1,c1
A16: o <> b by A5, ANALMETR:51;
A17: o <> c A18: o <> b1 o,b // o,c by A15, ANALMETR:def 11;
then o,c _|_ o,b1 by A5, A16, ANALMETR:84;
then o,b1 // o,c1 by A5, A17, ANALMETR:85;
then LIN o,b1,c1 by ANALMETR:def 11;
then LIN o',b1',c1' by ANALMETR:55;
then LIN b1',o',c1' by AFF_1:15;
then LIN b1,o,c1 by ANALMETR:55;
then A20: b1,o // b1,c1 by ANALMETR:def 11;
b1,o _|_ b,o by A5, ANALMETR:83;
then A21: b,o _|_ b1,c1 by A18, A20, ANALMETR:84;
LIN o',b',c' by A15, ANALMETR:55;
then LIN b',o',c' by AFF_1:15;
then LIN b,o,c by ANALMETR:55;
then b,o // b,c by ANALMETR:def 11;
hence b,c _|_ b1,c1 by A16, A21, ANALMETR:84; :: thesis: verum
end;
A22: now
assume A23: ( LIN a,b,c & not LIN o,b,c & o <> a1 ) ; :: thesis: b,c _|_ b1,c1
A24: a <> c A25: a <> b A26: a1 <> b1 by A5, A23, ANALMETR:85;
a,b // a,c by A23, ANALMETR:def 11;
then a,c _|_ a1,b1 by A5, A25, ANALMETR:84;
then a1,b1 // a1,c1 by A5, A24, ANALMETR:85;
then LIN a1,b1,c1 by ANALMETR:def 11;
then LIN a1',b1',c1' by ANALMETR:55;
then LIN b1',a1',c1' by AFF_1:15;
then LIN b1,a1,c1 by ANALMETR:55;
then A27: b1,a1 // b1,c1 by ANALMETR:def 11;
b1,a1 _|_ b,a by A5, ANALMETR:83;
then A28: b,a _|_ b1,c1 by A26, A27, ANALMETR:84;
LIN a',b',c' by A23, ANALMETR:55;
then LIN b',a',c' by AFF_1:15;
then LIN b,a,c by ANALMETR:55;
then b,a // b,c by ANALMETR:def 11;
hence b,c _|_ b1,c1 by A25, A28, ANALMETR:84; :: thesis: verum
end;
now
assume A29: ( not LIN a,b,c & not LIN o,b,c & o <> a1 ) ; :: thesis: b,c _|_ b1,c1
A30: ( o <> a & o <> b & o <> b1 & o <> c & o <> c1 & a <> c & a1 <> c1 )
proof
A31: o <> c A32: o <> b1 o <> c1 hence ( o <> a & o <> b & o <> b1 & o <> c & o <> c1 & a <> c & a1 <> c1 ) by A5, A31, A32, ANALMETR:51, ANALMETR:85; :: thesis: verum
end;
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
A35: ( o,b // o,p & o <> p ) by ANALMETR:51;
reconsider p' = p as Element of the carrier of (Af X) by ANALMETR:47;
consider p1 being Element of X such that
A36: ( a,c // a,p1 & a <> p1 ) by ANALMETR:51;
reconsider p1' = p1 as Element of the carrier of (Af X) by ANALMETR:47;
not o,p // a,p1 then not o',p' // a',p1' by ANALMETR:48;
then consider e' being Element of the carrier of (Af X) such that
A37: ( LIN o',p',e' & LIN a',p1',e' ) by AFF_1:74;
reconsider e = e' as Element of the carrier of X by ANALMETR:47;
LIN o,p,e by A37, ANALMETR:55;
then o,p // o,e by ANALMETR:def 11;
then o,e // o,b by A35, ANALMETR:82;
then A38: LIN o,e,b by ANALMETR:def 11;
LIN a,p1,e by A37, ANALMETR:55;
then a,p1 // a,e by ANALMETR:def 11;
then a,c // a,e by A36, ANALMETR:82;
then A39: LIN a,c,e by ANALMETR:def 11;
A40: c <> e
proof
assume c = e ; :: thesis: contradiction
then LIN o',c',b' by A38, ANALMETR:55;
then LIN o',b',c' by AFF_1:15;
hence contradiction by A29, ANALMETR:55; :: thesis: verum
end;
b <> e
proof
assume b = e ; :: thesis: contradiction
then LIN a',c',b' by A39, ANALMETR:55;
then LIN a',b',c' by AFF_1:15;
hence contradiction by A29, ANALMETR:55; :: thesis: verum
end;
hence ex e being Element of X st
( LIN o,e,b & LIN a,c,e & e <> c & e <> b ) by A38, A39, A40; :: thesis: verum
end;
then consider e being Element of X such that
A41: ( LIN o,e,b & LIN a,c,e & e <> c & e <> b ) ;
reconsider e' = e as Element of the carrier of (Af X) by ANALMETR:47;
ex e1 being Element of X st
( LIN o,e1,b1 & LIN a1,c1,e1 )
proof
consider p being Element of X such that
A42: ( o,b1 // o,p & o <> p ) by ANALMETR:51;
reconsider p' = p as Element of the carrier of (Af X) by ANALMETR:47;
consider p1 being Element of X such that
A43: ( a1,c1 // a1,p1 & a1 <> p1 ) by ANALMETR:51;
reconsider p1' = p1 as Element of the carrier of (Af X) by ANALMETR:47;
A44: not o,b1 // a1,c1 not o,p // a1,p1 then not o',p' // a1',p1' by ANALMETR:48;
then consider e1' being Element of the carrier of (Af X) such that
A45: ( LIN o',p',e1' & LIN a1',p1',e1' ) by AFF_1:74;
reconsider e1 = e1' as Element of the carrier of X by ANALMETR:47;
LIN o,p,e1 by A45, ANALMETR:55;
then o,p // o,e1 by ANALMETR:def 11;
then o,e1 // o,b1 by A42, ANALMETR:82;
then A46: LIN o,e1,b1 by ANALMETR:def 11;
LIN a1,p1,e1 by A45, ANALMETR:55;
then a1,p1 // a1,e1 by ANALMETR:def 11;
then a1,c1 // a1,e1 by A43, ANALMETR:82;
then LIN a1,c1,e1 by ANALMETR:def 11;
hence ex e1 being Element of X st
( LIN o,e1,b1 & LIN a1,c1,e1 ) by A46; :: thesis: verum
end;
then consider e1 being Element of X such that
A47: ( LIN o,e1,b1 & LIN a1,c1,e1 ) ;
reconsider e1' = e1 as Element of the carrier of (Af X) by ANALMETR:47;
A48: ( o,e _|_ o,e1 & o <> e & o <> e1 )
proof
A49: o,e _|_ o,e1 A51: o <> e
proof
assume o = e ; :: thesis: contradiction
then LIN a',c',o' by A41, ANALMETR:55;
then LIN o',c',a' by AFF_1:15;
then LIN o,c,a by ANALMETR:55;
hence contradiction by A5, ANALMETR:def 11; :: thesis: verum
end;
o <> e1
proof
assume o = e1 ; :: thesis: contradiction
then LIN a1',c1',o' by A47, ANALMETR:55;
then LIN o',a1',c1' by AFF_1:15;
then LIN o,a1,c1 by ANALMETR:55;
then o,a1 // o,c1 by ANALMETR:def 11;
then o,c1 _|_ o,a by A5, A29, ANALMETR:84;
hence contradiction by A5, A30, ANALMETR:85; :: thesis: verum
end;
hence ( o,e _|_ o,e1 & o <> e & o <> e1 ) by A49, A51; :: thesis: verum
end;
A52: not LIN o,a,e A54: e,a _|_ e1,a1 b,a _|_ b1,a1 by A5, ANALMETR:83;
then A56: e,e1 // b,b1 by A4, A5, A29, A30, A41, A47, A48, A52, A54, Def5;
A57: not LIN o,c,e e,c _|_ e1,c1 hence b,c _|_ b1,c1 by A3, A5, A30, A41, A47, A48, A56, A57, Def6; :: thesis: verum
end;
hence b,c _|_ b1,c1 by A7, A14, A22; :: thesis: verum
end;
then A60: ( not o,b // a,c implies b,c _|_ b1,c1 ) by A1, A2;
A61: now
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 A62: ( 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 ) ; :: thesis: ( not o,a // c,b implies b,c _|_ b1,c1 )
assume A63: not o,a // c,b ; :: thesis: b,c _|_ b1,c1
reconsider a' = a, a1' = a1, b' = b, b1' = b1, c' = c, c1' = c1, o' = o as Element of (Af X) by ANALMETR:47;
A64: now
assume A65: o = a1 ; :: thesis: b,c _|_ b1,c1
then A66: a1,b1 _|_ b,a1 by A62, ANALMETR:83;
A67: a1,b1 _|_ b,a by A62, ANALMETR:83;
not b,a1 // b,a
proof
assume b,a1 // b,a ; :: thesis: contradiction
then LIN b,o,a by A65, ANALMETR:def 11;
then LIN b',o',a' by ANALMETR:55;
then LIN o',a',b' by AFF_1:15;
then LIN o,a,b by ANALMETR:55;
hence contradiction by A62, ANALMETR:def 11; :: thesis: verum
end;
then A68: a1 = b1 by A66, A67, ANALMETR:85;
A69: a1,c1 _|_ c,a1 by A62, A65, ANALMETR:83;
a1,c1 _|_ c,a by A62, ANALMETR:83;
then A70: ( c,a1 // c,a or a1 = c1 ) by A69, ANALMETR:85;
not c,a1 // c,a
proof
assume c,a1 // c,a ; :: thesis: contradiction
then LIN c,o,a by A65, ANALMETR:def 11;
then LIN c',o',a' by ANALMETR:55;
then LIN o',c',a' by AFF_1:15;
then LIN o,c,a by ANALMETR:55;
hence contradiction by A62, ANALMETR:def 11; :: thesis: verum
end;
hence b,c _|_ b1,c1 by A68, A70, ANALMETR:51; :: thesis: verum
end;
A71: now
assume A72: ( LIN o,b,c & o <> a1 ) ; :: thesis: b,c _|_ b1,c1
A73: o <> b by A62, ANALMETR:51;
A74: o <> c A75: o <> b1 o,b // o,c by A72, ANALMETR:def 11;
then o,c _|_ o,b1 by A62, A73, ANALMETR:84;
then o,b1 // o,c1 by A62, A74, ANALMETR:85;
then LIN o,b1,c1 by ANALMETR:def 11;
then LIN o',b1',c1' by ANALMETR:55;
then LIN b1',o',c1' by AFF_1:15;
then LIN b1,o,c1 by ANALMETR:55;
then A77: b1,o // b1,c1 by ANALMETR:def 11;
b1,o _|_ b,o by A62, ANALMETR:83;
then A78: b,o _|_ b1,c1 by A75, A77, ANALMETR:84;
LIN o',b',c' by A72, ANALMETR:55;
then LIN b',o',c' by AFF_1:15;
then LIN b,o,c by ANALMETR:55;
then b,o // b,c by ANALMETR:def 11;
hence b,c _|_ b1,c1 by A73, A78, ANALMETR:84; :: thesis: verum
end;
A79: now
assume A80: ( LIN a,b,c & not LIN o,b,c & o <> a1 ) ; :: thesis: b,c _|_ b1,c1
A81: a <> c A82: a <> b A83: a1 <> b1 by A62, A80, ANALMETR:85;
a,b // a,c by A80, ANALMETR:def 11;
then a,c _|_ a1,b1 by A62, A82, ANALMETR:84;
then a1,b1 // a1,c1 by A62, A81, ANALMETR:85;
then LIN a1,b1,c1 by ANALMETR:def 11;
then LIN a1',b1',c1' by ANALMETR:55;
then LIN b1',a1',c1' by AFF_1:15;
then LIN b1,a1,c1 by ANALMETR:55;
then A84: b1,a1 // b1,c1 by ANALMETR:def 11;
b1,a1 _|_ b,a by A62, ANALMETR:83;
then A85: b,a _|_ b1,c1 by A83, A84, ANALMETR:84;
LIN a',b',c' by A80, ANALMETR:55;
then LIN b',a',c' by AFF_1:15;
then LIN b,a,c by ANALMETR:55;
then b,a // b,c by ANALMETR:def 11;
hence b,c _|_ b1,c1 by A82, A85, ANALMETR:84; :: thesis: verum
end;
now
assume A86: ( not LIN a,b,c & not LIN o,b,c & o <> a1 ) ; :: thesis: b,c _|_ b1,c1
A87: ( o <> a & o <> b & o <> c & o <> b1 & o <> c1 & a <> a1 & a <> b & a1 <> b1 & a <> c & a1 <> c1 )
proof
A88: o <> a by A62, ANALMETR:51;
A89: o <> c A90: o <> b1 o <> c1 hence ( o <> a & o <> b & o <> c & o <> b1 & o <> c1 & a <> a1 & a <> b & a1 <> b1 & a <> c & a1 <> c1 ) by A62, A88, A89, A90, ANALMETR:51, ANALMETR:85; :: thesis: verum
end;
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
A93: ( o,a // o,p & o <> p ) by ANALMETR:51;
reconsider p' = p as Element of (Af X) by ANALMETR:47;
consider p1 being Element of X such that
A94: ( b,c // b,p1 & b <> p1 ) by ANALMETR:51;
reconsider p1' = p1 as Element of (Af X) by ANALMETR:47;
not o,p // b,p1 then not o',p' // b',p1' by ANALMETR:48;
then consider e' being Element of (Af X) such that
A95: ( LIN o',p',e' & LIN b',p1',e' ) by AFF_1:74;
reconsider e = e' as Element of X by ANALMETR:47;
LIN o,p,e by A95, ANALMETR:55;
then A96: o,p // o,e by ANALMETR:def 11;
then o,e // o,a by A93, ANALMETR:82;
then A97: LIN o,e,a by ANALMETR:def 11;
LIN b,p1,e by A95, ANALMETR:55;
then b,p1 // b,e by ANALMETR:def 11;
then b,c // b,e by A94, ANALMETR:82;
then A98: LIN b,c,e by ANALMETR:def 11;
A99: c <> e by A62, A93, A96, ANALMETR:82;
A100: b <> e
proof
assume b = e ; :: thesis: contradiction
then LIN o',b',a' by A97, ANALMETR:55;
then LIN o',a',b' by AFF_1:15;
then LIN o,a,b by ANALMETR:55;
hence contradiction by A62, ANALMETR:def 11; :: thesis: verum
end;
a <> e
proof
assume a = e ; :: thesis: contradiction
then LIN b',c',a' by A98, ANALMETR:55;
then LIN a',b',c' by AFF_1:15;
hence contradiction by A86, ANALMETR:55; :: 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 A97, A98, A99, A100; :: thesis: verum
end;
then consider e being Element of X such that
A101: ( LIN b,c,e & LIN o,e,a & e <> b & c <> e & a <> e ) ;
reconsider e' = e as Element of (Af X) by ANALMETR:47;
ex e1 being Element of X st
( LIN o,e1,a1 & e,e1 // a,a1 )
proof
consider p being Element of X such that
A102: ( o,a1 // o,p & o <> p ) by ANALMETR:51;
reconsider p' = p as Element of (Af X) by ANALMETR:47;
consider p1 being Element of X such that
A103: ( a,a1 // e,p1 & e <> p1 ) by ANALMETR:51;
reconsider p1' = p1 as Element of (Af X) by ANALMETR:47;
not o,p // e,p1 then not o',p' // e',p1' by ANALMETR:48;
then consider e1' being Element of (Af X) such that
A105: ( LIN o',p',e1' & LIN e',p1',e1' ) by AFF_1:74;
reconsider e1 = e1' as Element of X by ANALMETR:47;
LIN o,p,e1 by A105, ANALMETR:55;
then o,p // o,e1 by ANALMETR:def 11;
then o,e1 // o,a1 by A102, ANALMETR:82;
then A106: LIN o,e1,a1 by ANALMETR:def 11;
LIN e,p1,e1 by A105, ANALMETR:55;
then e,p1 // e,e1 by ANALMETR:def 11;
then e,e1 // a,a1 by A103, ANALMETR:82;
hence ex e1 being Element of X st
( LIN o,e1,a1 & e,e1 // a,a1 ) by A106; :: thesis: verum
end;
then consider e1 being Element of X such that
A107: ( LIN o,e1,a1 & e,e1 // a,a1 ) ;
reconsider e1' = e1 as Element of (Af X) by ANALMETR:47;
A108: ( o,e _|_ o,e1 & o <> e & o <> e1 )
proof
A109: o,e _|_ o,e1 A111: o <> e
proof
assume o = e ; :: thesis: contradiction
then LIN b',c',o' by A101, ANALMETR:55;
then LIN o',b',c' by AFF_1:15;
hence contradiction by A86, ANALMETR:55; :: thesis: verum
end;
o <> e1 hence ( o,e _|_ o,e1 & o <> e & o <> e1 ) by A109, A111; :: thesis: verum
end;
A115: not LIN o,b,a o,e // o,a by A101, ANALMETR:def 11;
then o',e' // o',a' by ANALMETR:48;
then o',a' // o',e' by AFF_1:13;
then o,a // o,e by ANALMETR:48;
then A116: LIN o,a,e by ANALMETR:def 11;
o,e1 // o,a1 by A107, ANALMETR:def 11;
then o',e1' // o',a1' by ANALMETR:48;
then o',a1' // o',e1' by AFF_1:13;
then o,a1 // o,e1 by ANALMETR:48;
then A117: LIN o,a1,e1 by ANALMETR:def 11;
e',e1' // a',a1' by A107, ANALMETR:48;
then a',a1' // e',e1' by AFF_1:13;
then A118: a,a1 // e,e1 by ANALMETR:48;
then A119: e,b _|_ e1,b1 by A3, A62, A86, A87, A101, A108, A115, A116, A117, Def6;
not LIN o,c,a by A62, ANALMETR:def 11;
then A120: e,c _|_ e1,c1 by A3, A62, A86, A87, A101, A108, A116, A117, A118, Def6;
A121: ( e1 <> c1 & e1 <> b1 ) A123: c,e _|_ c1,e1 by A120, ANALMETR:83;
A124: LIN b',c',e' by A101, ANALMETR:55;
then LIN c',e',b' by AFF_1:15;
then LIN c,e,b by ANALMETR:55;
then c,e // c,b by ANALMETR:def 11;
then A125: c,b _|_ c1,e1 by A101, A123, ANALMETR:84;
A126: c <> b
proof
assume c = b ; :: thesis: contradiction
then LIN o',b',c' by AFF_1:16;
hence contradiction by A86, ANALMETR:55; :: thesis: verum
end;
b',c' // b',e' by A124, AFF_1:def 1;
then c',b' // e',b' by AFF_1:13;
then c,b // e,b by ANALMETR:48;
then e,b _|_ c1,e1 by A125, A126, ANALMETR:84;
then e1,b1 // c1,e1 by A101, A119, ANALMETR:85;
then e1',b1' // c1',e1' by ANALMETR:48;
then e1',b1' // e1',c1' by AFF_1:13;
then LIN e1',b1',c1' by AFF_1:def 1;
then LIN b1',e1',c1' by AFF_1:15;
then b1',e1' // b1',c1' by AFF_1:def 1;
then e1',b1' // b1',c1' by AFF_1:13;
then A127: e1,b1 // b1,c1 by ANALMETR:48;
LIN b',e',c' by A124, AFF_1:15;
then b',e' // b',c' by AFF_1:def 1;
then e',b' // b',c' by AFF_1:13;
then e,b // b,c by ANALMETR:48;
then e1,b1 _|_ b,c by A101, A119, ANALMETR:84;
hence b,c _|_ b1,c1 by A121, A127, ANALMETR:84; :: thesis: verum
end;
hence b,c _|_ b1,c1 by A64, A71, A79; :: thesis: verum
end;
then A128: ( not o,a // c,b implies b,c _|_ b1,c1 ) by A2;
now
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 A129: ( 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 ) ; :: thesis: ( o,a // c,b & o,b // a,c implies b,c _|_ b1,c1 )
assume A130: ( o,a // c,b & o,b // a,c ) ; :: thesis: b,c _|_ b1,c1
reconsider a' = a, b' = b, c' = c, o' = o as Element of (Af X) by ANALMETR:47;
A131: now
assume A132: o = a1 ; :: thesis: b,c _|_ b1,c1
then A133: a1,b1 _|_ b,a1 by A129, ANALMETR:83;
A134: a1,b1 _|_ b,a by A129, ANALMETR:83;
not b,a1 // b,a then A135: a1 = b1 by A133, A134, ANALMETR:85;
A136: a1,c1 _|_ c,a1 by A129, A132, ANALMETR:83;
a1,c1 _|_ c,a by A129, ANALMETR:83;
then A137: ( c,a1 // c,a or a1 = c1 ) by A136, ANALMETR:85;
not c,a1 // c,a hence b,c _|_ b1,c1 by A135, A137, ANALMETR:51; :: thesis: verum
end;
A138: now
assume A139: ( o,a1 // c1,b1 & o <> a1 ) ; :: thesis: b,c _|_ b1,c1
o <> a
proof
assume o = a ; :: thesis: contradiction
then LIN o',c',a' by AFF_1:16;
then LIN o,c,a by ANALMETR:55;
hence contradiction by A129, ANALMETR:def 11; :: thesis: verum
end;
then c,b _|_ o,a1 by A129, A130, ANALMETR:84;
then c,b _|_ c1,b1 by A139, ANALMETR:84;
hence b,c _|_ b1,c1 by ANALMETR:83; :: thesis: verum
end;
now
assume A140: ( not o,a1 // c1,b1 & o <> a1 ) ; :: thesis: b,c _|_ b1,c1
A141: ( o,a1 _|_ o,a & o,b1 _|_ o,b & o,c1 _|_ o,c & a1,b1 _|_ a,b & a1,c1 _|_ a,c ) by A129, ANALMETR:83;
A142: not o,c1 // o,a1 not o,a1 // o,b1 then b1,c1 _|_ b,c by A61, A140, A141, A142;
hence b,c _|_ b1,c1 by ANALMETR:83; :: thesis: verum
end;
hence b,c _|_ b1,c1 by A131, A138; :: thesis: verum
end;
hence b,c _|_ b1,c1 by A1, A2, A60, A128; :: thesis: verum