let AFP be AffinPlane; :: thesis: ( AFP is Moufangian iff for o being Element of
for K being Subset of
for c, c', a, b, a', b' being Element of 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
for K being Subset of
for c, c', a, b, a', b' being Element of 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
for K being Subset of
for c, c', a, b, a', b' being Element of 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
for K being Subset of
for c, c', a, b, a', b' being Element of 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 ; :: thesis: for K being Subset of
for c, c', a, b, a', b' being Element of 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 ; :: thesis: for c, c', a, b, a', b' being Element of 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 ; :: 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 that
A2: o in K and
A3: c in K and
A4: c' in K and
A5: K is being_line and
A6: LIN o,a,a' and
A7: LIN o,b,b' and
A8: not a in K and
A9: a,b // K and
A10: a',b' // K and
A11: a,c // a',c' ; :: thesis: b,c // b',c'
A12: a,b // a',b' by A5, A9, A10, AFF_1:45;

A13: now

A14: now

assume A15: a = b ; :: thesis: b,c // b',c'

A16: now

A17: not o,a // K by A2, A8, AFF_1:48, AFF_1:49;
A18: LIN o,b',b by A7, AFF_1:15;
assume that
A19: a',o // K and
A20: a' <> b' ; :: thesis: contradiction
o,a // o,a' by A6, AFF_1:def 1;
then a',o // o,a by AFF_1:13;
then A21: ( o,a // K or a' = o ) by A19, AFF_1:46;
then b' in K by A2, A5, A8, A10, AFF_1:37;
hence contradiction by A2, A5, A8, A15, A20, A21, A17, A18, AFF_1:39; :: thesis: verum

end;

LIN o,a,o by AFF_1:16;
then LIN a',b',o by A2, A6, A7, A8, A15, AFF_1:17;
then a',b' // a',o by AFF_1:def 1;
hence b,c // b',c' by A10, A11, A15, A16, AFF_1:46; :: thesis: verum

end;

assume o <> c ; :: thesis: b,c // b',c'
hence b,c // b',c' by A1, A2, A3, A4, A5, A6, A7, A8, A9, A11, A12, A14, AFF_2:def 7; :: thesis: verum

end;

now

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

end;

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

end;

assume A26: for o being Element of
for K being Subset of
for c, c', a, b, a', b' being Element of 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 ; :: thesis: 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 & 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 ; :: 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 that
A27: K is being_line and
A28: o in K and
A29: c in K and
A30: c' in K and
A31: not a in K and
o <> c and
A32: a <> b and
A33: LIN o,a,a' and
A34: LIN o,b,b' and
A35: a,b // a',b' and
A36: a,c // a',c' and
A37: a,b // K ; :: thesis: b,c // b',c'
a',b' // K by A32, A35, A37, AFF_1:46;
hence b,c // b',c' by A26, A27, A28, A29, A30, A31, A33, A34, A36, A37; :: thesis: verum

end;

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