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

proof

let K be Subset of AFP; :: thesis: for o, a, b, c, a9, b9, c9 being Element of AFP st K is being_line & o in K & c in K & c9 in K & not a in K & a <> b & LIN o,a,a9 & a,b // a9,b9 & b,c // b9,c9 & a,c // a9,c9 & a,b // K holds
LIN o,b,b9
let o, a, b, c, a9, b9, c9 be Element of AFP; :: thesis: ( K is being_line & o in K & c in K & c9 in K & not a in K & a <> b & LIN o,a,a9 & a,b // a9,b9 & b,c // b9,c9 & a,c // a9,c9 & a,b // K implies LIN o,b,b9 )
assume that
A2: K is being_line and
A3: o in K and
A4: c in K and
A5: c9 in K and
A6: not a in K and
A7: a <> b and
A8: LIN o,a,a9 and
A9: a,b // a9,b9 and
A10: b,c // b9,c9 and
A11: a,c // a9,c9 and
A12: a,b // K ; :: thesis: LIN o,b,b9
consider P being Subset of AFP such that
A13: a9 in P and
A14: K // P by A2, AFF_1:49;
A15: P is being_line by A14, AFF_1:36;
set A = Line (o,b);
set C = Line (o,a);
A16: o in Line (o,b) by AFF_1:15;
A17: b in Line (o,b) by AFF_1:15;
assume A18: not LIN o,b,b9 ; :: thesis: contradiction
then o <> b by AFF_1:7;
then A19: Line (o,b) is being_line by AFF_1:def 3;
A20: not b in K by A6, A12, AFF_1:35;
not Line (o,b) // P

proof

assume Line (o,b) // P ; :: thesis: contradiction
then Line (o,b) // K by A14, AFF_1:44;
hence contradiction by A3, A20, A16, A17, AFF_1:45; :: thesis: verum

end;

then consider x being Element of AFP such that
A21: x in Line (o,b) and
A22: x in P by A19, A15, AFF_1:58;
A23: o in Line (o,a) by AFF_1:15;
a,b // P by A12, A14, AFF_1:43;
then a9,b9 // P by A7, A9, AFF_1:32;
then A24: b9 in P by A13, A15, AFF_1:23;
then A25: LIN b9,x,b9 by A15, A22, AFF_1:21;
A26: a in Line (o,a) by AFF_1:15;
A27: LIN o,b,x by A19, A16, A17, A21, AFF_1:21;
A28: Line (o,a) is being_line by A3, A6, AFF_1:def 3;
then A29: a9 in Line (o,a) by A3, A6, A8, A23, A26, AFF_1:25;
A30: b9 <> c9

proof

A31: a9,c9 // c,a by A11, AFF_1:4;
assume A32: b9 = c9 ; :: thesis: contradiction
then P = K by A5, A14, A24, AFF_1:45;
then a9 = o by A2, A3, A6, A28, A23, A26, A29, A13, AFF_1:18;
then b9 = o by A2, A3, A4, A5, A6, A32, A31, AFF_1:48;
hence contradiction by A18, AFF_1:7; :: thesis: verum

end;

A33: a9 <> b9

proof

assume A34: a9 = b9 ; :: thesis: contradiction

A35: now :: thesis: not a9 = c9

assume a9 = c9 ; :: thesis: contradiction
then b9 = o by A2, A3, A5, A6, A28, A23, A26, A29, A34, AFF_1:18;
hence contradiction by A18, AFF_1:7; :: thesis: verum

end;

( a,c // b,c or a9 = c9 ) by A10, A11, A34, AFF_1:5;
then c,a // c,b by A35, AFF_1:4;
then LIN c,a,b by AFF_1:def 1;
then LIN a,c,b by AFF_1:6;
then a,c // a,b by AFF_1:def 1;
then a,b // a,c by AFF_1:4;
then a,c // K by A7, A12, AFF_1:32;
then c,a // K by AFF_1:34;
hence contradiction by A2, A4, A6, AFF_1:23; :: thesis: verum

end;

A36: b <> c by A4, A6, A12, AFF_1:35;
a9,x // K by A13, A14, A22, AFF_1:40;
then b,c // x,c9 by A1, A2, A3, A4, A5, A6, A8, A11, A12, A27, Lm2;
then b9,c9 // x,c9 by A10, A36, AFF_1:5;
then c9,b9 // c9,x by AFF_1:4;
then LIN c9,b9,x by AFF_1:def 1;
then A37: LIN b9,x,c9 by AFF_1:6;
LIN b9,x,a9 by A13, A15, A22, A24, AFF_1:21;
then LIN b9,c9,a9 by A18, A27, A37, A25, AFF_1:8;
then b9,c9 // b9,a9 by AFF_1:def 1;
then b9,c9 // a9,b9 by AFF_1:4;
then b,c // a9,b9 by A10, A30, AFF_1:5;
then a,b // b,c by A9, A33, AFF_1:5;
then b,c // K by A7, A12, AFF_1:32;
then c,b // K by AFF_1:34;
hence contradiction by A2, A4, A20, AFF_1:23; :: thesis: verum

end;