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