let OAS be OAffinSpace; :: thesis: for p, a, a', b, b' being Element of 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 ; :: 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'
consider c being Element of such that
A5: Mid a,p,c and
A6: p <> c by DIRAF:17;
A7: a,p // p,c by A5, DIRAF:def 3;
A8: a <> p by A1, DIRAF:37;
then consider c' being Element of such that
A9: a',p // p,c' and
A10: a',a // c,c' by A7, ANALOAF:def 5;
A11: a',a '||' c',c by A10, DIRAF:def 4;
A12: c <> c'

proof

assume c = c' ; :: thesis: contradiction
then Mid a',p,c by A9, DIRAF:def 3;
then LIN a',p,c by DIRAF:34;
then A13: LIN p,c,a' by DIRAF:36;
LIN a,p,c by A5, DIRAF:34;
then A14: LIN p,c,a by DIRAF:36;
LIN p,c,p by DIRAF:37;
hence contradiction by A1, A6, A14, A13, DIRAF:38; :: thesis: verum

end;

p,a // c,p by A7, DIRAF:5;
then c,p // p,b by A2, A8, ANALOAF:def 5;
then consider b'' being Element of such that
A15: c',p // p,b'' and
A16: c',c // b,b'' by A6, ANALOAF:def 5;
A17: a',a '||' b,b' by A4, DIRAF:27;
A18: p <> c'

proof

assume p = c' ; :: thesis: contradiction
then a',a '||' c,p by A10, DIRAF:def 4;
then A19: p,c '||' a,a' by DIRAF:27;
a,p '||' p,c by A7, DIRAF:def 4;
then a,p '||' a,a' by A6, A19, DIRAF:28;
then LIN a,p,a' by DIRAF:def 5;
hence contradiction by A1, DIRAF:36; :: thesis: verum

end;

p,a '||' p,b by A2, DIRAF:def 4;
then A20: LIN p,a,b by DIRAF:def 5;
A21: c',c // a,a' by A10, DIRAF:5;
a',p '||' p,c' by A9, DIRAF:def 4;
then A22: p,a' '||' p,c' by DIRAF:27;
p,a' '||' p,b' by A3, DIRAF:def 4;
then A23: LIN p,a',b' by DIRAF:def 5;
c',p '||' p,b'' by A15, DIRAF:def 4;
then p,c' '||' p,b'' by DIRAF:27;
then p,a' '||' p,b'' by A18, A22, DIRAF:28;
then A24: LIN p,a',b'' by DIRAF:def 5;
c',c '||' b,b'' by A16, DIRAF:def 4;
then A25: a',a '||' b,b'' by A12, A11, DIRAF:28;
not LIN p,a',a by A1, DIRAF:36;
then c',c // b,b' by A20, A23, A17, A16, A24, A25, Th11;
hence a,a' // b,b' by A12, A21, ANALOAF:def 5; :: thesis: verum