let OAS be OAffinSpace; :: thesis: for a, b, c, p being Element of OAS st p,b // p,c & b <> p holds
ex x being Element of OAS st
( p,a // p,x & b,a // c,x )
let a, b, c, p be Element of OAS; :: thesis: ( p,b // p,c & b <> p implies ex x being Element of OAS st
( p,a // p,x & b,a // c,x ) )
assume that
A1: p,b // p,c and
A2: b <> p ; :: thesis: ex x being Element of OAS st
( p,a // p,x & b,a // c,x )
A3: b,p // c,p by A1, DIRAF:2;
A4: now :: thesis: ( p <> c & p <> a implies ex x being Element of OAS st
( p,a // p,x & b,a // c,x ) )
assume that
p <> c and
A5: p <> a ; :: thesis: ex x being Element of OAS st
( p,a // p,x & b,a // c,x )
consider e1 being Element of OAS such that
A6: Mid a,p,e1 and
A7: p <> e1 by DIRAF:13;
a,p // p,e1 by A6, DIRAF:def 3;
then consider e2 being Element of OAS such that
A8: b,p // p,e2 and
A9: b,a // e1,e2 by A5, ANALOAF:def 5;
Mid e1,p,a by A6, DIRAF:9;
then A10: e1,p // p,a by DIRAF:def 3;
A11: now :: thesis: ( p = e2 implies ex x being Element of OAS st
( p,a // p,x & b,a // c,x ) )
A12: now :: thesis: ( a,b // b,p implies ex x being Element of OAS st
( p,a // p,x & b,a // c,x ) )
A13: now :: thesis: ( b,p // a,p implies ( p,a // p,c & b,a // c,c ) )
assume b,p // a,p ; :: thesis: ( p,a // p,c & b,a // c,c )
then a,p // c,p by A2, A3, ANALOAF:def 5;
hence ( p,a // p,c & b,a // c,c ) by DIRAF:2, DIRAF:4; :: thesis: verum
end;
assume A14: a,b // b,p ; :: thesis: ex x being Element of OAS st
( p,a // p,x & b,a // c,x )
then a,b // a,p by ANALOAF:def 5;
then ( b,p // a,p or a = b ) by A14, ANALOAF:def 5;
hence ex x being Element of OAS st
( p,a // p,x & b,a // c,x ) by A13, DIRAF:1; :: thesis: verum
end;
A15: now :: thesis: ( a,p // p,b implies ( p,a // p,p & b,a // c,p ) )
assume A16: a,p // p,b ; :: thesis: ( p,a // p,p & b,a // c,p )
then a,p // a,b by ANALOAF:def 5;
then a,b // p,b by A5, A16, ANALOAF:def 5;
then b,a // b,p by DIRAF:2;
hence ( p,a // p,p & b,a // c,p ) by A2, A3, DIRAF:3, DIRAF:4; :: thesis: verum
end;
assume p = e2 ; :: thesis: ex x being Element of OAS st
( p,a // p,x & b,a // c,x )
then b,a // p,a by A7, A10, A9, DIRAF:3;
then a,b // a,p by DIRAF:2;
hence ex x being Element of OAS st
( p,a // p,x & b,a // c,x ) by A12, A15, DIRAF:6; :: thesis: verum
end;
A17: now :: thesis: ( e1 = e2 & e2 <> p implies ex x being Element of OAS st
( p,a // p,x & b,a // c,x ) )
A18: now :: thesis: ( p,a // a,b & p,c // c,a implies ( p,a // p,c & b,a // c,c ) )
assume that
p,a // a,b and
A19: p,c // c,a ; :: thesis: ( p,a // p,c & b,a // c,c )
p,c // p,a by A19, ANALOAF:def 5;
hence ( p,a // p,c & b,a // c,c ) by DIRAF:2, DIRAF:4; :: thesis: verum
end;
A20: now :: thesis: ( p,b // b,a & p,c // c,a implies ( p,a // p,c & b,a // c,c ) )
assume that
p,b // b,a and
A21: p,c // c,a ; :: thesis: ( p,a // p,c & b,a // c,c )
p,c // p,a by A21, ANALOAF:def 5;
hence ( p,a // p,c & b,a // c,c ) by DIRAF:2, DIRAF:4; :: thesis: verum
end;
A22: now :: thesis: ( p,a // a,b & p,a // a,c implies ( p,a // p,a & b,a // c,a ) )
assume that
A23: p,a // a,b and
A24: p,a // a,c ; :: thesis: ( p,a // p,a & b,a // c,a )
a,b // a,c by A5, A23, A24, ANALOAF:def 5;
hence ( p,a // p,a & b,a // c,a ) by DIRAF:1, DIRAF:2; :: thesis: verum
end;
A25: ( p,b // b,a & p,a // a,c implies ( p,a // p,c & b,a // c,c ) ) by ANALOAF:def 5;
assume that
A26: e1 = e2 and
A27: e2 <> p ; :: thesis: ex x being Element of OAS st
( p,a // p,x & b,a // c,x )
p,e2 // a,p by A10, A26, DIRAF:2;
then b,p // a,p by A8, A27, DIRAF:3;
then A28: p,b // p,a by DIRAF:2;
then p,a // p,c by A1, A2, ANALOAF:def 5;
hence ex x being Element of OAS st
( p,a // p,x & b,a // c,x ) by A28, A25, A20, A22, A18, DIRAF:6; :: thesis: verum
end;
now :: thesis: ( e1 <> e2 & e2 <> p implies ex x being Element of OAS st
( p,a // p,x & b,a // c,x ) )
assume that
A29: e1 <> e2 and
A30: e2 <> p ; :: thesis: ex x being Element of OAS st
( p,a // p,x & b,a // c,x )
p,b // e2,p by A8, DIRAF:2;
then e2,p // p,c by A1, A2, ANALOAF:def 5;
then consider x being Element of OAS such that
A31: e1,p // p,x and
A32: e1,e2 // c,x by A30, ANALOAF:def 5;
A33: p,a // p,x by A7, A10, A31, ANALOAF:def 5;
b,a // c,x by A9, A29, A32, DIRAF:3;
hence ex x being Element of OAS st
( p,a // p,x & b,a // c,x ) by A33; :: thesis: verum
end;
hence ex x being Element of OAS st
( p,a // p,x & b,a // c,x ) by A17, A11; :: thesis: verum
end;
A34: ( p = c implies ( p,a // p,c & b,a // c,c ) ) by DIRAF:4;
( p = a implies ( p,a // p,a & b,a // c,a ) ) by A1, DIRAF:1, DIRAF:2;
hence ex x being Element of OAS st
( p,a // p,x & b,a // c,x ) by A34, A4; :: thesis: verum