let OAS be OAffinSpace; :: thesis: Lambda OAS is Fanoian

set AS = Lambda OAS;

for a, b, c, d being Element of (Lambda OAS) st a,b // c,d & a,c // b,d & a,d // b,c holds

a,b // a,c

set AS = Lambda OAS;

for a, b, c, d being Element of (Lambda OAS) st a,b // c,d & a,c // b,d & a,d // b,c holds

a,b // a,c

proof

hence
Lambda OAS is Fanoian
; :: thesis: verum
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

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

end;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

proof

( a1,b1 '||' c1,d1 & a1,c1 '||' b1,d1 )
by A1, A2, DIRAF:38;
assume
a1,b1,c1 are_collinear
; :: thesis: contradiction

then a1,b1 '||' a1,c1 by DIRAF:def 5;

hence contradiction by A4, DIRAF:38; :: thesis: verum

end;then a1,b1 '||' a1,c1 by DIRAF:def 5;

hence contradiction by A4, DIRAF:38; :: thesis: verum

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