let OAS be OAffinSpace; :: thesis: for p, a, a', b, b' being Element of OAS st not LIN p,a,a' & p,a // p,b & p,a' // p,b' & a,a' '||' b,b' holds
a,a' // b,b'
let p, a, a', b, b' be Element of OAS; :: thesis: ( not LIN p,a,a' & p,a // p,b & p,a' // p,b' & a,a' '||' b,b' implies a,a' // b,b' )
assume that
A1: not LIN p,a,a' and
A2: p,a // p,b and
A3: p,a' // p,b' and
A4: a,a' '||' b,b' ; :: thesis: a,a' // b,b'
A5: not LIN p,a',a by A1, DIRAF:36;
p,a '||' p,b by A2, DIRAF:def 4;
then A6: LIN p,a,b by DIRAF:def 5;
p,a' '||' p,b' by A3, DIRAF:def 4;
then A7: LIN p,a',b' by DIRAF:def 5;
A8: a',a '||' b,b' by A4, DIRAF:27;
consider c being Element of OAS such that
A9: ( Mid a,p,c & p <> c ) by DIRAF:17;
A10: a,p // p,c by A9, DIRAF:def 3;
A11: a <> p by A1, DIRAF:37;
then consider c' being Element of OAS such that
A12: a',p // p,c' and
A13: a',a // c,c' by A10, ANALOAF:def 5;
A14: c <> c'

proof

assume c = c' ; :: thesis: contradiction
then Mid a',p,c by A12, DIRAF:def 3;
then LIN a',p,c by DIRAF:34;
then ( LIN a,p,c & LIN p,c,a' ) by A9, DIRAF:34, DIRAF:36;
then ( LIN p,c,p & LIN p,c,a & LIN p,c,a' ) by DIRAF:36, DIRAF:37;
hence contradiction by A1, A9, DIRAF:38; :: thesis: verum

end;

A15: p <> c'

proof

assume p = c' ; :: thesis: contradiction
then a',a '||' c,p by A13, DIRAF:def 4;
then ( a,p '||' p,c & p,c '||' a,a' ) by A10, DIRAF:27, DIRAF:def 4;
then a,p '||' a,a' by A9, DIRAF:28;
then LIN a,p,a' by DIRAF:def 5;
hence contradiction by A1, DIRAF:36; :: thesis: verum

end;

p,a // c,p by A10, DIRAF:5;
then c,p // p,b by A2, A11, ANALOAF:def 5;
then consider b'' being Element of OAS such that
A16: c',p // p,b'' and
A17: c',c // b,b'' by A9, ANALOAF:def 5;
a',p '||' p,c' by A12, DIRAF:def 4;
then ( p,a' '||' p,c' & c',p '||' p,b'' ) by A16, DIRAF:27, DIRAF:def 4;
then ( p,a' '||' p,c' & p,c' '||' p,b'' ) by DIRAF:27;
then p,a' '||' p,b'' by A15, DIRAF:28;
then A18: LIN p,a',b'' by DIRAF:def 5;
( a',a '||' c',c & c',c '||' b,b'' ) by A13, A17, DIRAF:def 4;
then a',a '||' b,b'' by A14, DIRAF:28;
then ( c',c // a,a' & c',c // b,b' ) by A5, A6, A7, A8, A13, A17, A18, Th11, DIRAF:5;
hence a,a' // b,b' by A14, ANALOAF:def 5; :: thesis: verum