let OAS be OAffinSpace; :: thesis: for o, a, b, a9, b9 being Element of OAS st not o,a,b are_collinear & a,o // o,a9 & o,b,b9 are_collinear & a,b '||' a9,b9 holds
( b,o // o,b9 & a,b // b9,a9 )
let o, a, b, a9, b9 be Element of OAS; :: thesis: ( not o,a,b are_collinear & a,o // o,a9 & o,b,b9 are_collinear & a,b '||' a9,b9 implies ( b,o // o,b9 & a,b // b9,a9 ) )
assume that
A1: not o,a,b are_collinear and
A2: a,o // o,a9 and
A3: o,b,b9 are_collinear and
A4: a,b '||' a9,b9 ; :: thesis: ( b,o // o,b9 & a,b // b9,a9 )
( Mid a,o,a9 & a,b '||' b9,a9 ) by A2, A4, DIRAF:22, DIRAF:def 3;
then Mid b,o,b9 by A1, A3, PASCH:6;
hence b,o // o,b9 by DIRAF:def 3; :: thesis: a,b // b9,a9
hence a,b // b9,a9 by A1, A2, A4, PASCH:12; :: thesis: verum