let OAS be OAffinSpace; 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; ( 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
; ( 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; a,b // b9,a9
hence
a,b // b9,a9
by A1, A2, A4, PASCH:12; verum