let OAS be OAffinSpace; :: thesis: for o, a, b, a9, b9 being Element of OAS st not LIN o,a,b & a,o // o,a9 & LIN o,b,b9 & 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 LIN o,a,b & a,o // o,a9 & LIN o,b,b9 & a,b '||' a9,b9 implies ( b,o // o,b9 & a,b // b9,a9 ) )
assume that
A1: not LIN o,a,b and
A2: a,o // o,a9 and
A3: LIN o,b,b9 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