let AFP be AffinPlane; :: thesis: ( AFP is Moufangian implies for K being Subset of AFP
for o, a, b, c, a', b', c' being Element of AFP 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' )
assume A1: AFP is Moufangian ; :: thesis: for K being Subset of AFP
for o, a, b, c, a', b', c' being Element of AFP 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'
thus for K being Subset of AFP
for o, a, b, c, a', b', c' being Element of AFP 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: verum

proof

let K be Subset of AFP; :: thesis: for o, a, b, c, a', b', c' being Element of AFP 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'
let o, a, b, c, a', b', c' be Element of AFP; :: thesis: ( 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 implies LIN o,b,b' )
assume that
A2: K is being_line and
A3: ( o in K & c in K & c' in K ) and
A4: not a in K and
A5: ( a <> b & LIN o,a,a' & a,b // a',b' & b,c // b',c' & a,c // a',c' & a,b // K ) ; :: thesis: LIN o,b,b'
assume A6: not LIN o,b,b' ; :: thesis: contradiction
A7: not b in K by A4, A5, AFF_1:49;
A8: b <> c by A3, A4, A5, AFF_1:49;
A9: ( o <> b & o <> a ) by A3, A4, A6, AFF_1:16;
set A = Line o,b;
set C = Line o,a;
A10: ( Line o,b is being_line & Line o,a is being_line & o in Line o,b & b in Line o,b & o in Line o,a & a in Line o,a ) by A9, AFF_1:26, AFF_1:def 3;
then A11: a' in Line o,a by A3, A4, A5, AFF_1:39;
consider P being Subset of AFP such that
A12: ( a' in P & K // P ) by A2, AFF_1:63;
A13: ( P is being_line & P // K ) by A12, AFF_1:50;
not Line o,b // P

proof

assume Line o,b // P ; :: thesis: contradiction
then Line o,b // K by A12, AFF_1:58;
hence contradiction by A3, A7, A10, AFF_1:59; :: thesis: verum

end;

then consider x being Element of AFP such that
A14: ( x in Line o,b & x in P ) by A10, A13, AFF_1:72;
A15: LIN o,b,x by A10, A14, AFF_1:33;
a',x // K by A12, A14, AFF_1:54;
then b,c // x,c' by A1, A2, A3, A4, A5, A15, Lm2;
then b',c' // x,c' by A5, A8, AFF_1:14;
then c',b' // c',x by AFF_1:13;
then LIN c',b',x by AFF_1:def 1;
then A16: LIN b',x,c' by AFF_1:15;
a,b // P by A5, A12, AFF_1:57;
then a',b' // P by A5, AFF_1:46;
then A17: b' in P by A12, A13, AFF_1:37;
then ( LIN b',x,a' & LIN b',x,b' ) by A12, A13, A14, AFF_1:33;
then LIN b',c',a' by A6, A15, A16, AFF_1:17;
then b',c' // b',a' by AFF_1:def 1;
then A18: b',c' // a',b' by AFF_1:13;
A19: b' <> c'

proof

assume A20: b' = c' ; :: thesis: contradiction
then P = K by A3, A12, A17, AFF_1:59;
then A21: a' = o by A2, A3, A4, A10, A11, A12, AFF_1:30;
a',c' // c,a by A5, AFF_1:13;
then b' = o by A2, A3, A4, A20, A21, AFF_1:62;
hence contradiction by A6, AFF_1:16; :: thesis: verum

end;

A22: a' <> b'

proof

assume A23: a' = b' ; :: thesis: contradiction
then A24: ( a,c // b,c or a' = c' ) by A5, AFF_1:14;

now

assume a' = c' ; :: thesis: contradiction
then b' = o by A2, A3, A4, A10, A11, A23, AFF_1:30;
hence contradiction by A6, AFF_1:16; :: thesis: verum

end;

then c,a // c,b by A24, 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 A5, AFF_1:46;
then c,a // K by AFF_1:48;
hence contradiction by A2, A3, A4, AFF_1:37; :: thesis: verum

end;

b,c // a',b' by A5, A18, A19, AFF_1:14;
then a,b // b,c by A5, A22, AFF_1:14;
then b,c // K by A5, AFF_1:46;
then c,b // K by AFF_1:48;
hence contradiction by A2, A3, A7, AFF_1:37; :: thesis: verum

end;