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