let AFP be AffinPlane; :: thesis: ( AFP is Moufangian iff for o being Element of AFP
for K being Subset of AFP
for c, c', a, b, a', b' being Element of AFP st o in K & c in K & c' in K & K is being_line & LIN o,a,a' & LIN o,b,b' & not a in K & a,b // K & a',b' // K & a,c // a',c' holds
b,c // b',c' )
thus ( AFP is Moufangian implies for o being Element of AFP
for K being Subset of AFP
for c, c', a, b, a', b' being Element of AFP st o in K & c in K & c' in K & K is being_line & LIN o,a,a' & LIN o,b,b' & not a in K & a,b // K & a',b' // K & a,c // a',c' holds
b,c // b',c' ) :: thesis: ( ( for o being Element of AFP
for K being Subset of AFP
for c, c', a, b, a', b' being Element of AFP st o in K & c in K & c' in K & K is being_line & LIN o,a,a' & LIN o,b,b' & not a in K & a,b // K & a',b' // K & a,c // a',c' holds
b,c // b',c' ) implies AFP is Moufangian )

proof

assume A1: AFP is Moufangian ; :: thesis: for o being Element of AFP
for K being Subset of AFP
for c, c', a, b, a', b' being Element of AFP st o in K & c in K & c' in K & K is being_line & LIN o,a,a' & LIN o,b,b' & not a in K & a,b // K & a',b' // K & a,c // a',c' holds
b,c // b',c'
let o be Element of AFP; :: thesis: for K being Subset of AFP
for c, c', a, b, a', b' being Element of AFP st o in K & c in K & c' in K & K is being_line & LIN o,a,a' & LIN o,b,b' & not a in K & a,b // K & a',b' // K & a,c // a',c' holds
b,c // b',c'
let K be Subset of AFP; :: thesis: for c, c', a, b, a', b' being Element of AFP st o in K & c in K & c' in K & K is being_line & LIN o,a,a' & LIN o,b,b' & not a in K & a,b // K & a',b' // K & a,c // a',c' holds
b,c // b',c'
let c, c', a, b, a', b' be Element of AFP; :: thesis: ( o in K & c in K & c' in K & K is being_line & LIN o,a,a' & LIN o,b,b' & not a in K & a,b // K & a',b' // K & a,c // a',c' implies b,c // b',c' )
assume A2: ( o in K & c in K & c' in K & K is being_line & LIN o,a,a' & LIN o,b,b' & not a in K & a,b // K & a',b' // K & a,c // a',c' ) ; :: thesis: b,c // b',c'
then A3: a,b // a',b' by AFF_1:45;

A4: now

assume A5: o = c ; :: thesis: b,c // b',c'
then LIN a,c,a' by A2, AFF_1:15;
then LIN a,c,c' by A2, AFF_1:18;
then A6: LIN c,c',a by AFF_1:15;
then A7: c = c' by A2, AFF_1:39;
( LIN c,b,b' & LIN c',b,b' ) by A2, A5, A6, AFF_1:39;
then ( LIN b,b',c & LIN b',b,c' ) by AFF_1:15;
then ( b,b' // b,c & b',b // b',c' ) by AFF_1:def 1;
then A8: ( b,b' // b,c & b,b' // b',c' ) by AFF_1:13;
( b = b' implies b,c // b',c' ) by A7, AFF_1:11;
hence b,c // b',c' by A8, AFF_1:14; :: thesis: verum

end;

now

assume A9: o <> c ; :: thesis: b,c // b',c'

now

assume A10: a = b ; :: thesis: b,c // b',c'
then ( LIN o,a,a' & LIN o,a,b' & LIN o,a,o ) by A2, AFF_1:16;
then LIN a',b',o by A2, AFF_1:17;
then A11: a',b' // a',o by AFF_1:def 1;

now

assume A12: ( a',o // K & a' <> b' ) ; :: thesis: contradiction
o,a // o,a' by A2, AFF_1:def 1;
then a',o // o,a by AFF_1:13;
then A13: ( o,a // K or a' = o ) by A12, AFF_1:46;
A14: not o,a // K by A2, AFF_1:48, AFF_1:49;
A15: b' in K by A2, A13, AFF_1:37;
LIN o,b',b by A2, AFF_1:15;
hence contradiction by A2, A10, A12, A13, A14, A15, AFF_1:39; :: thesis: verum

end;

hence b,c // b',c' by A2, A10, A11, AFF_1:46; :: thesis: verum

end;

hence b,c // b',c' by A1, A2, A3, A9, AFF_2:def 7; :: thesis: verum

end;

hence b,c // b',c' by A4; :: thesis: verum

end;

assume A16: for o being Element of AFP
for K being Subset of AFP
for c, c', a, b, a', b' being Element of AFP st o in K & c in K & c' in K & K is being_line & LIN o,a,a' & LIN o,b,b' & not a in K & a,b // K & a',b' // K & a,c // a',c' holds
b,c // b',c' ; :: thesis: AFP is Moufangian

now

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 & o <> c & a <> b & LIN o,a,a' & LIN o,b,b' & a,b // a',b' & a,c // a',c' & a,b // K holds
b,c // b',c'
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 & o <> c & a <> b & LIN o,a,a' & LIN o,b,b' & a,b // a',b' & a,c // a',c' & a,b // K implies b,c // b',c' )
assume A17: ( K is being_line & o in K & c in K & c' in K & not a in K & o <> c & a <> b & LIN o,a,a' & LIN o,b,b' & a,b // a',b' & a,c // a',c' & a,b // K ) ; :: thesis: b,c // b',c'
then a',b' // K by AFF_1:46;
hence b,c // b',c' by A16, A17; :: thesis: verum

end;

hence AFP is Moufangian by AFF_2:def 7; :: thesis: verum