let OAS be OAffinSpace; for a, b, c, d1, d2 being Element of OAS st not a,b,c are_collinear & a,b '||' c,d1 & a,b '||' c,d2 & a,c '||' b,d1 & a,c '||' b,d2 holds
d1 = d2
let a, b, c, d1, d2 be Element of OAS; ( not a,b,c are_collinear & a,b '||' c,d1 & a,b '||' c,d2 & a,c '||' b,d1 & a,c '||' b,d2 implies d1 = d2 )
assume that
A1:
not a,b,c are_collinear
and
A2:
a,b '||' c,d1
and
A3:
a,b '||' c,d2
and
A4:
a,c '||' b,d1
and
A5:
a,c '||' b,d2
; d1 = d2
assume A6:
d1 <> d2
; contradiction
a <> c
by A1, DIRAF:31;
then
b,d1 '||' b,d2
by A4, A5, DIRAF:23;
then
b,d1,d2 are_collinear
by DIRAF:def 5;
then A7:
d1,d2,b are_collinear
by DIRAF:30;
A9:
d1,d2,d1 are_collinear
by DIRAF:31;
a <> b
by A1, DIRAF:31;
then
c,d1 '||' c,d2
by A2, A3, DIRAF:23;
then A10:
c,d1,d2 are_collinear
by DIRAF:def 5;
then A11:
d1,d2,c are_collinear
by DIRAF:30;
d1,d2,c are_collinear
by A10, DIRAF:30;
then
d1,d2 '||' c,d1
by A9, DIRAF:34;
then
( d1,d2 '||' a,b or c = d1 )
by A2, DIRAF:23;
then
d1,d2 '||' b,a
by A8, DIRAF:22;
then
d1,d2,a are_collinear
by A6, A7, DIRAF:33;
hence
contradiction
by A1, A6, A11, A7, DIRAF:32; verum