let OAS be OAffinSpace; :: thesis: 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; :: thesis: ( 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 ; :: thesis: d1 = d2
assume A6: d1 <> d2 ; :: thesis: 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;
A8: now :: thesis: not c = d1
assume c = d1 ; :: thesis: contradiction
then c,a '||' c,b by A4, DIRAF:22;
then c,a,b are_collinear by DIRAF:def 5;
hence contradiction by A1, DIRAF:30; :: thesis: verum
end;
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; :: thesis: verum