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

proof

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 & a,c // b,d ) and
A2: a,d // b,c ; :: thesis: a,b // a,c
assume A3: not a,b // a,c ; :: thesis: contradiction
then A4: not LIN a,b,c by AFF_1:def 1;
reconsider a1 = a, b1 = b, c1 = c, d1 = d as Element of OAS by Th2;
A5: ( a1,b1 '||' c1,d1 & a1,c1 '||' b1,d1 ) by A1, DIRAF:45;
not LIN a1,b1,c1

proof

assume LIN a1,b1,c1 ; :: thesis: contradiction
then a1,b1 '||' a1,c1 by DIRAF:def 5;
hence contradiction by A3, DIRAF:45; :: thesis: verum

end;

then consider x1 being Element of OAS such that
A6: ( LIN x1,a1,d1 & LIN x1,b1,c1 ) by A5, PASCH:33;
reconsider x = x1 as Element of (Lambda OAS) by Th2;
A7: ( LIN a,d,x & LIN b,c,x )

proof

( x1,a1 '||' x1,d1 & x1,b1 '||' x1,c1 ) by A6, DIRAF:def 5;
then ( x,a // x,d & x,b // x,c ) by DIRAF:45;
then ( LIN x,a,d & LIN x,b,c ) by AFF_1:def 1;
hence ( LIN a,d,x & LIN b,c,x ) by AFF_1:15; :: thesis: verum

end;

set P = Line a,d;
set Q = Line b,c;
A8: b <> c by A4, AFF_1:16;
A9: a <> d by A1, A3, AFF_1:13;
then A10: ( Line a,d is being_line & Line b,c is being_line ) by A8, AFF_1:def 3;
A11: ( a in Line a,d & d in Line a,d & x in Line a,d ) by A7, AFF_1:26, AFF_1:def 2;
A12: ( b in Line b,c & c in Line b,c & x in Line b,c ) by A7, AFF_1:26, AFF_1:def 2;
then Line a,d // Line b,c by A2, A8, A9, A10, A11, AFF_1:52;
then Line a,d = Line b,c by A11, A12, AFF_1:59;
hence contradiction by A4, A10, A11, A12, AFF_1:33; :: thesis: verum

end;

hence Lambda OAS is Fanoian by Def5; :: thesis: verum