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