let AFP be AffinPlane; :: thesis: for a, b, p, p9, q, q9, x, y being Element of AFP
for K being Subset of AFP st a,b // K & not a in K & not x in K & AFP is Moufangian & p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K & q in K & q9 in K & q,a // q9,x holds
q,b // q9,y
let a, b, p, p9, q, q9, x, y be Element of AFP; :: thesis: for K being Subset of AFP st a,b // K & not a in K & not x in K & AFP is Moufangian & p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K & q in K & q9 in K & q,a // q9,x holds
q,b // q9,y
let K be Subset of AFP; :: thesis: ( a,b // K & not a in K & not x in K & AFP is Moufangian & p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K & q in K & q9 in K & q,a // q9,x implies q,b // q9,y )
assume that
A1: a,b // K and
A2: not a in K and
A3: not x in K and
A4: AFP is Moufangian and
A5: p in K and
A6: p9 in K and
A7: p,a // p9,x and
A8: p,b // p9,y and
A9: x,y // K and
A10: q in K and
A11: q9 in K and
A12: q,a // q9,x ; :: thesis: q,b // q9,y
A13: K is being_line by A1, AFF_1:26;
A14: now :: thesis: ( not a,x // K & a <> b implies q,b // q9,y )
A15: a,q // x,q9 by A12, AFF_1:4;
A16: b,p // y,p9 by A8, AFF_1:4;
A17: a,p // x,p9 by A7, AFF_1:4;
set A = Line (a,x);
assume that
A18: not a,x // K and
A19: a <> b ; :: thesis: q,b // q9,y
a <> x by A13, A18, AFF_1:33;
then A20: Line (a,x) is being_line by AFF_1:def 3;
A21: x in Line (a,x) by AFF_1:15;
A22: a in Line (a,x) by AFF_1:15;
then consider o being Element of AFP such that
A23: o in Line (a,x) and
A24: o in K by A13, A18, A21, A20, AFF_1:40, AFF_1:58;
A25: LIN o,a,x by A22, A21, A20, A23, AFF_1:21;
K is being_line by A1, AFF_1:26;
then a,b // x,y by A1, A9, AFF_1:31;
then LIN o,b,y by A1, A2, A4, A5, A6, A19, A24, A25, A17, A16, Lm3, AFF_1:26;
then b,q // y,q9 by A1, A2, A4, A9, A10, A11, A13, A24, A25, A15, Lm2;
hence q,b // q9,y by AFF_1:4; :: thesis: verum
end;
A26: now :: thesis: ( a,x // K & a <> b & p <> q implies q,b // q9,y )
set M = Line (a,b);
assume that
A27: a,x // K and
A28: a <> b and
A29: p <> q ; :: thesis: q,b // q9,y
A30: Line (a,b) is being_line by A28, AFF_1:def 3;
K is being_line by A1, AFF_1:26;
then a,b // a,x by A1, A27, AFF_1:31;
then LIN a,b,x by AFF_1:def 1;
then A31: x in Line (a,b) by AFF_1:def 2;
A32: b in Line (a,b) by AFF_1:15;
A33: a in Line (a,b) by AFF_1:15;
A34: Line (a,b) // K by A1, A28, AFF_1:def 5;
then x,y // Line (a,b) by A9, AFF_1:43;
then y in Line (a,b) by A30, A31, AFF_1:23;
hence q,b // q9,y by A4, A5, A6, A7, A8, A10, A11, A12, A28, A29, A33, A32, A34, A31, Th7; :: thesis: verum
end;
A35: ( a = b implies x = y )
proof
set M = Line (x,y);
A36: x in Line (x,y) by AFF_1:15;
assume a = b ; :: thesis: x = y
then p9,x // p9,y by A2, A5, A7, A8, AFF_1:5;
then LIN p9,x,y by AFF_1:def 1;
then LIN x,y,p9 by AFF_1:6;
then A37: p9 in Line (x,y) by AFF_1:def 2;
assume x <> y ; :: thesis: contradiction
then Line (x,y) // K by A9, AFF_1:def 5;
hence contradiction by A3, A6, A36, A37, AFF_1:45; :: thesis: verum
end;
now :: thesis: ( p = q implies q,b // q9,y )
assume A38: p = q ; :: thesis: q,b // q9,y
p9 = q9
proof
p9,x // q9,x by A2, A5, A7, A12, A38, AFF_1:5;
then x,p9 // x,q9 by AFF_1:4;
then LIN x,p9,q9 by AFF_1:def 1;
then A39: LIN p9,q9,x by AFF_1:6;
assume p9 <> q9 ; :: thesis: contradiction
hence contradiction by A1, A3, A6, A11, A39, AFF_1:25, AFF_1:26; :: thesis: verum
end;
hence q,b // q9,y by A8, A38; :: thesis: verum
end;
hence q,b // q9,y by A12, A35, A14, A26; :: thesis: verum