let a, b, c, d be Element of (Lambda OAS); :: thesis: ( a,b // c,d & a,c // b,d & a,d // b,c implies a,b // a,c )
assume that
A1: a,b // c,d and
A2: a,c // b,d and
A3: a,d // b,c ; :: thesis: a,b // a,c
reconsider a1 = a, b1 = b, c1 = c, d1 = d as Element of OAS by Th1;
set P = Line (a,d);
set Q = Line (b,c);
assume A4: not a,b // a,c ; :: thesis: contradiction
then A5: a <> d by A1, AFF_1:4;
then A6: Line (a,d) is being_line by AFF_1:def 3;
A7: not a1,b1,c1 are_collinear ( a1,b1 '||' c1,d1 & a1,c1 '||' b1,d1 ) by A1, A2, DIRAF:38;
then consider x1 being Element of OAS such that
A8: x1,a1,d1 are_collinear and
A9: x1,b1,c1 are_collinear by A7, PASCH:25;
reconsider x = x1 as Element of (Lambda OAS) by Th1;
A10: d in Line (a,d) by AFF_1:15;
x1,a1 '||' x1,d1 by A8, DIRAF:def 5;
then x,a // x,d by DIRAF:38;
then LIN x,a,d by AFF_1:def 1;
then LIN a,d,x by AFF_1:6;
then A11: x in Line (a,d) by AFF_1:def 2;
A12: ( a in Line (a,d) & b in Line (b,c) ) by AFF_1:15;
x1,b1 '||' x1,c1 by A9, DIRAF:def 5;
then x,b // x,c by DIRAF:38;
then LIN x,b,c by AFF_1:def 1;
then LIN b,c,x by AFF_1:6;
then A13: x in Line (b,c) by AFF_1:def 2;
A14: c in Line (b,c) by AFF_1:15;
A15: not LIN a,b,c by A4, AFF_1:def 1;
then A16: b <> c by AFF_1:7;
then Line (b,c) is being_line by AFF_1:def 3;
then Line (a,d) // Line (b,c) by A3, A16, A5, A6, A10, A12, A14, AFF_1:38;
then Line (a,d) = Line (b,c) by A11, A13, AFF_1:45;
hence contradiction by A15, A6, A12, A14, AFF_1:21; :: thesis: verum