let OAS be OAffinSpace; for a, a9, b, b9, p being Element of OAS st not p,a,b are_collinear & a,p // p,a9 & b,p // p,b9 & a,b '||' a9,b9 holds
a,b // b9,a9
let a, a9, b, b9, p be Element of OAS; ( not p,a,b are_collinear & a,p // p,a9 & b,p // p,b9 & a,b '||' a9,b9 implies a,b // b9,a9 )
assume that
A1:
not p,a,b are_collinear
and
A2:
a,p // p,a9
and
A3:
b,p // p,b9
and
A4:
a,b '||' a9,b9
; a,b // b9,a9
A5:
not p,b,a are_collinear
by A1, DIRAF:30;
Mid b,p,b9
by A3, DIRAF:def 3;
then
b,p,b9 are_collinear
by DIRAF:28;
then A6:
p,b,b9 are_collinear
by DIRAF:30;
Mid a,p,a9
by A2, DIRAF:def 3;
then
a,p,a9 are_collinear
by DIRAF:28;
then A7:
p,a,a9 are_collinear
by DIRAF:30;
A8:
b,a '||' a9,b9
by A4, DIRAF:22;
a <> p
by A1, DIRAF:31;
then consider q being Element of OAS such that
A9:
b,p // p,q
and
A10:
b,a // a9,q
by A2, ANALOAF:def 5;
Mid b,p,q
by A9, DIRAF:def 3;
then
b,p,q are_collinear
by DIRAF:28;
then A11:
p,b,q are_collinear
by DIRAF:30;
b,a '||' a9,q
by A10, DIRAF:def 4;
then
b,a // a9,b9
by A10, A5, A7, A6, A11, A8, Th4;
hence
a,b // b9,a9
by DIRAF:2; verum