let AFP be AffinPlane; :: thesis: ( AFP is Moufangian implies for K, A, C being Subset of
for p, q, a, a', b, b' being Element of st K // A & K // C & K <> A & K <> C & p in K & q in K & a in A & a' in A & b in C & b' in C & p,a // q,a' & p,b // q,b' holds
a,b // a',b' )
assume AFP is Moufangian ; :: thesis: for K, A, C being Subset of
for p, q, a, a', b, b' being Element of st K // A & K // C & K <> A & K <> C & p in K & q in K & a in A & a' in A & b in C & b' in C & p,a // q,a' & p,b // q,b' holds
a,b // a',b'
then A1: AFP is translational by AFF_2:28;
let K, A, C be Subset of ; :: thesis: for p, q, a, a', b, b' being Element of st K // A & K // C & K <> A & K <> C & p in K & q in K & a in A & a' in A & b in C & b' in C & p,a // q,a' & p,b // q,b' holds
a,b // a',b'
let p, q, a, a', b, b' be Element of ; :: thesis: ( K // A & K // C & K <> A & K <> C & p in K & q in K & a in A & a' in A & b in C & b' in C & p,a // q,a' & p,b // q,b' implies a,b // a',b' )
assume that
A2: K // A and
A3: K // C and
A4: K <> A and
A5: K <> C and
A6: p in K and
A7: q in K and
A8: a in A and
A9: a' in A and
A10: b in C and
A11: b' in C and
A12: p,a // q,a' and
A13: p,b // q,b' ; :: thesis: a,b // a',b'
A14: A is being_line by A2, AFF_1:50;
A15: C is being_line by A3, AFF_1:50;
K is being_line by A2, AFF_1:50;
hence a,b // a',b' by A2, A3, A4, A5, A6, A7, A8, A9, A10, A11, A12, A13, A1, A14, A15, AFF_2:def 11; :: thesis: verum