let AFP be AffinPlane; :: thesis:
assume A1: AFP is Moufangian ; :: thesis:
thus for K being Subset of
for o, a, b, c, a', b', c' being Element of st K is being_line & o in K & c in K & c' in K & not a in K & a <> b & LIN o,a,a' & a,b // a',b' & b,c // b',c' & a,c // a',c' & a,b // K holds
LIN o,b,b' :: thesis:

proof

let K be Subset of ; :: thesis:
let o, a, b, c, a', b', c' be Element of ; :: thesis:
assume that
A2: K is being_line and
A3: o in K and
A4: c in K and
A5: c' in K and
A6: not a in K and
A7: a <> b and
A8: LIN o,a,a' and
A9: a,b // a',b' and
A10: b,c // b',c' and
A11: a,c // a',c' and
A12: a,b // K ; :: thesis:
consider P being Subset of such that
A13: a' in P and
A14: K // P by A2, AFF_1:63;
A15: P is being_line by A14, AFF_1:50;
set A = Line o,b;
set C = Line o,a;
A16: o in Line o,b by AFF_1:26;
A17: b in Line o,b by AFF_1:26;
assume A18: not LIN o,b,b' ; :: thesis:
then o <> b by AFF_1:16;
then A19: Line o,b is being_line by AFF_1:def 3;
A20: not b in K by A6, A12, AFF_1:49;
not Line o,b // P

proof

assume Line o,b // P ; :: thesis:
then Line o,b // K by A14, AFF_1:58;
hence contradiction by A3, A20, A16, A17, AFF_1:59; :: thesis:

end;

then consider x being Element of such that
A21: x in Line o,b and
A22: x in P by A19, A15, AFF_1:72;
A23: o in Line o,a by AFF_1:26;
a,b // P by A12, A14, AFF_1:57;
then a',b' // P by A7, A9, AFF_1:46;
then A24: b' in P by A13, A15, AFF_1:37;
then A25: LIN b',x,b' by A15, A22, AFF_1:33;
A26: a in Line o,a by AFF_1:26;
A27: LIN o,b,x by A19, A16, A17, A21, AFF_1:33;
A28: Line o,a is being_line by A3, A6, AFF_1:def 3;
then A29: a' in Line o,a by A3, A6, A8, A23, A26, AFF_1:39;
A30: b' <> c'

proof

A31: a',c' // c,a by A11, AFF_1:13;
assume A32: b' = c' ; :: thesis:
then P = K by A5, A14, A24, AFF_1:59;
then a' = o by A2, A3, A6, A28, A23, A26, A29, A13, AFF_1:30;
then b' = o by A2, A3, A4, A5, A6, A32, A31, AFF_1:62;
hence contradiction by A18, AFF_1:16; :: thesis:

end;

A33: a' <> b'

proof

assume A34: a' = b' ; :: thesis:

A35: now

assume a' = c' ; :: thesis:
then b' = o by A2, A3, A5, A6, A28, A23, A26, A29, A34, AFF_1:30;
hence contradiction by A18, AFF_1:16; :: thesis:

end;

( a,c // b,c or a' = c' ) by A10, A11, A34, AFF_1:14;
then c,a // c,b by A35, AFF_1:13;
then LIN c,a,b by AFF_1:def 1;
then LIN a,c,b by AFF_1:15;
then a,c // a,b by AFF_1:def 1;
then a,b // a,c by AFF_1:13;
then a,c // K by A7, A12, AFF_1:46;
then c,a // K by AFF_1:48;
hence contradiction by A2, A4, A6, AFF_1:37; :: thesis:

end;

A36: b <> c by A4, A6, A12, AFF_1:49;
a',x // K by A13, A14, A22, AFF_1:54;
then b,c // x,c' by A1, A2, A3, A4, A5, A6, A8, A11, A12, A27, Lm2;
then b',c' // x,c' by A10, A36, AFF_1:14;
then c',b' // c',x by AFF_1:13;
then LIN c',b',x by AFF_1:def 1;
then A37: LIN b',x,c' by AFF_1:15;
LIN b',x,a' by A13, A15, A22, A24, AFF_1:33;
then LIN b',c',a' by A18, A27, A37, A25, AFF_1:17;
then b',c' // b',a' by AFF_1:def 1;
then b',c' // a',b' by AFF_1:13;
then b,c // a',b' by A10, A30, AFF_1:14;
then a,b // b,c by A9, A33, AFF_1:14;
then b,c // K by A7, A12, AFF_1:46;
then c,b // K by AFF_1:48;
hence contradiction by A2, A4, A20, AFF_1:37; :: thesis:

end;