let V be RealLinearSpace; :: thesis:
let OAS be OAffinSpace; :: thesis:
assume A1: OAS = OASpace V ; :: thesis:
set AS = Lambda OAS;
for M, N being Subset of (Lambda OAS)
for o, a, b, c, a9, b9, c9 being Element of (Lambda OAS) st M is being_line & N is being_line & M <> N & o in M & o in N & o <> a & o <> a9 & o <> b & o <> b9 & o <> c & o <> c9 & a in M & b in M & c in M & a9 in N & b9 in N & c9 in N & a,b9 // b,a9 & b,c9 // c,b9 holds
a,c9 // c,a9

proof

let M, N be Subset of (Lambda OAS); :: thesis:
let o, a, b, c, a9, b9, c9 be Element of (Lambda OAS); :: thesis:
assume that
A2: M is being_line and
A3: N is being_line and
A4: M <> N and
A5: o in M and
A6: o in N and
A7: o <> a and
A8: o <> a9 and
A9: o <> b and
o <> b9 and
A10: o <> c and
A11: o <> c9 and
A12: a in M and
A13: b in M and
A14: c in M and
A15: a9 in N and
A16: b9 in N and
A17: c9 in N and
A18: a,b9 // b,a9 and
A19: b,c9 // c,b9 ; :: thesis:
reconsider o1 = o, a1 = a, b1 = b, c1 = c, a19 = a9, b19 = b9, c19 = c9 as Element of OAS by Th1;
reconsider q = o1, u = a1, v = b1, w = c1, u9 = a19, v9 = b19, w9 = c19 as VECTOR of V by A1, Th3;
b1,c19 '||' c1,b19 by A19, DIRAF:38;
then A20: v,w9 '||' w,v9 by A1, Th4;
A21: ( not q,v '||' q,w9 & not q,v '||' q,u9 )

proof

assume ( q,v '||' q,w9 or q,v '||' q,u9 ) ; :: thesis:
then ( o1,b1 '||' o1,c19 or o1,b1 '||' o1,a19 ) by A1, Th4;
then ( o,b // o,c9 or o,b // o,a9 ) by DIRAF:38;
then ( LIN o,b,c9 or LIN o,b,a9 ) by AFF_1:def 1;
then ( c9 in M or a9 in M ) by A2, A5, A9, A13, AFF_1:25;
hence contradiction by A2, A3, A4, A5, A6, A8, A11, A15, A17, AFF_1:18; :: thesis:

end;

LIN o,c,b by A2, A5, A13, A14, AFF_1:21;
then o,c // o,b by AFF_1:def 1;
then o1,c1 '||' o1,b1 by DIRAF:38;
then q,w '||' q,v by A1, Th4;
then consider r2 being Real such that
A22: w - q = r2 * (v - q) and
A23: r2 <> 0 by A9, A10, Lm2;
A24: - r2 <> 0 by A23;
LIN o,a,b by A2, A5, A12, A13, AFF_1:21;
then o,a // o,b by AFF_1:def 1;
then o1,a1 '||' o1,b1 by DIRAF:38;
then q,u '||' q,v by A1, Th4;
then consider r1 being Real such that
A25: u - q = r1 * (v - q) and
A26: r1 <> 0 by A7, A9, Lm2;
A27: (- r1) * (q - v) = r1 * (- (q - v)) by RLVECT_1:24
.= u - q by A25, RLVECT_1:33 ;
LIN o,c9,b9 by A3, A6, A16, A17, AFF_1:21;
then o,c9 // o,b9 by AFF_1:def 1;
then o1,c19 '||' o1,b19 by DIRAF:38;
then A28: q,w9 '||' q,v9 by A1, Th4;
(- r2) * (q - v) = r2 * (- (q - v)) by RLVECT_1:24
.= w - q by A22, RLVECT_1:33 ;
then A29: q - v = ((- r2) ") * (w - q) by A24, ANALOAF:5;
(- r2) " <> 0 by A24, XCMPLX_1:202;
then v9 = q + (((- ((- r2) ")) ") * (w9 - q)) by A20, A29, A28, A21, Th10
.= q + (((- (- (r2 "))) ") * (w9 - q)) by XCMPLX_1:222
.= q + (r2 * (w9 - q)) ;
then A30: v9 - q = r2 * (w9 - q) by RLSUB_2:61;
LIN o,a9,b9 by A3, A6, A15, A16, AFF_1:21;
then o,a9 // o,b9 by AFF_1:def 1;
then o1,a19 '||' o1,b19 by DIRAF:38;
then A31: q,u9 '||' q,v9 by A1, Th4;
a1,b19 '||' b1,a19 by A18, DIRAF:38;
then b1,a19 '||' a1,b19 by DIRAF:22;
then A32: v,u9 '||' u,v9 by A1, Th4;
r1 " <> 0 by A26, XCMPLX_1:202;
then A33: (r1 ") * r2 <> 0 by A23, XCMPLX_1:6;
set s = r1 * (r2 ");
A34: u - q = r1 * ((r2 ") * (w - q)) by A25, A22, A23, ANALOAF:6
.= (r1 * (r2 ")) * (w - q) by RLVECT_1:def 7 ;
- r1 <> 0 by A26;
then A35: (- r1) " <> 0 by XCMPLX_1:202;
- r1 <> 0 by A26;
then q - v = ((- r1) ") * (u - q) by A27, ANALOAF:6;
then v9 = q + (((- ((- r1) ")) ") * (u9 - q)) by A32, A35, A31, A21, Th10
.= q + (((- (- (r1 "))) ") * (u9 - q)) by XCMPLX_1:222
.= q + (r1 * (u9 - q)) ;
then v9 - q = r1 * (u9 - q) by RLSUB_2:61;
then u9 - q = (r1 ") * (r2 * (w9 - q)) by A26, A30, ANALOAF:6
.= ((r1 ") * r2) * (w9 - q) by RLVECT_1:def 7 ;
then A36: w9 - q = (((r1 ") * r2) ") * (u9 - q) by A33, ANALOAF:6
.= (((r1 ") ") * (r2 ")) * (u9 - q) by XCMPLX_1:204
.= (r1 * (r2 ")) * (u9 - q) ;
1 * (w9 - u) = w9 - u by RLVECT_1:def 8
.= ((r1 * (r2 ")) * (u9 - q)) - ((r1 * (r2 ")) * (w - q)) by A36, A34, Lm3
.= (r1 * (r2 ")) * ((u9 - q) - (w - q)) by RLVECT_1:34
.= (r1 * (r2 ")) * (u9 - w) by Lm3 ;
then ( u,w9 // w,u9 or u,w9 // u9,w ) by ANALMETR:14;
then u,w9 '||' w,u9 by GEOMTRAP:def 1;
then a1,c19 '||' c1,a19 by A1, Th4;
hence a,c9 // c,a9 by DIRAF:38; :: thesis:

end;

hence Lambda OAS is Pappian by AFF_2:def 2; :: thesis: