let OAS be OAffinSpace; :: thesis: for o, a, b, a', b' being Element of the carrier 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' )
A5: Mid a,o,a' by A2, DIRAF:def 3;
a,b '||' b',a' by A4, DIRAF:27;
then Mid b,o,b' by A1, A3, A5, 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