let AFP be AffinPlane; :: thesis: for a, b, p, p9, q, q9, x, y being Element of AFP
for M, K being Subset of AFP st K // M & p in K & q in K & p9 in K & q9 in K & AFP is Moufangian & a in M & b in M & x in M & y in M & a <> b & q <> p & p,a // p9,x & p,b // p9,y & q,a // q9,x holds
q,b // q9,y
let a, b, p, p9, q, q9, x, y be Element of AFP; :: thesis: for M, K being Subset of AFP st K // M & p in K & q in K & p9 in K & q9 in K & AFP is Moufangian & a in M & b in M & x in M & y in M & a <> b & q <> p & p,a // p9,x & p,b // p9,y & q,a // q9,x holds
q,b // q9,y
let M, K be Subset of AFP; :: thesis: ( K // M & p in K & q in K & p9 in K & q9 in K & AFP is Moufangian & a in M & b in M & x in M & y in M & a <> b & q <> p & p,a // p9,x & p,b // p9,y & q,a // q9,x implies q,b // q9,y )
assume that
A1: K // M and
A2: p in K and
A3: q in K and
A4: p9 in K and
A5: q9 in K and
A6: AFP is Moufangian and
A7: a in M and
A8: b in M and
A9: x in M and
A10: y in M and
A11: a <> b and
A12: q <> p and
A13: p,a // p9,x and
A14: p,b // p9,y and
A15: q,a // q9,x ; :: thesis: q,b // q9,y
A16: K is being_line by A1, AFF_1:36;
A17: M is being_line by A1, AFF_1:36;
now :: thesis: ( K <> M implies q,b // q9,y )
set D9 = Line (q9,x);
set B99 = Line (p9,y);
set D = Line (q,a);
set B9 = Line (p,b);
A18: q in Line (q,a) by AFF_1:15;
A19: a in Line (q,a) by AFF_1:15;
A20: x in Line (q9,x) by AFF_1:15;
A21: q9 in Line (q9,x) by AFF_1:15;
A22: LIN p,q,q9 by A2, A3, A5, A16, AFF_1:21;
A23: LIN p,q,p9 by A2, A3, A4, A16, AFF_1:21;
assume A24: K <> M ; :: thesis: q,b // q9,y
then A25: q9 <> x by A1, A5, A9, AFF_1:45;
A26: not a in K by A1, A7, A24, AFF_1:45;
A27: b <> p by A1, A2, A8, A24, AFF_1:45;
then A28: Line (p,b) is being_line by AFF_1:def 3;
A29: not q in M by A1, A3, A24, AFF_1:45;
A30: not p in M by A1, A2, A24, AFF_1:45;
A31: LIN a,b,x by A7, A8, A9, A17, AFF_1:21;
A32: now :: thesis: ( ( for a, b, c being Element of AFP holds
( not LIN a,b,c or not a <> b or not a <> c or not b <> c ) ) implies q,b // q9,y )
A33: now :: thesis: ( q = p9 implies not q = q9 )
assume that
A34: q = p9 and
A35: q = q9 ; :: thesis: contradiction
LIN q,a,x by A15, A35, AFF_1:def 1;
then LIN a,x,q by AFF_1:6;
then a = x by A7, A9, A17, A29, AFF_1:25;
then a,q // a,p by A13, A34, AFF_1:4;
then LIN a,q,p by AFF_1:def 1;
then LIN p,q,a by AFF_1:6;
hence contradiction by A2, A3, A12, A16, A26, AFF_1:25; :: thesis: verum
end;
A36: now :: thesis: ( p = p9 implies not p = q9 )
assume that
A37: p = p9 and
A38: p = q9 ; :: thesis: contradiction
LIN p,a,x by A13, A37, AFF_1:def 1;
then LIN a,x,p by AFF_1:6;
then a = x by A7, A9, A17, A30, AFF_1:25;
then a,q // a,q9 by A15, AFF_1:4;
then LIN a,q,q9 by AFF_1:def 1;
then LIN p,q,a by A38, AFF_1:6;
hence contradiction by A2, A3, A12, A16, A26, AFF_1:25; :: thesis: verum
end;
assume A39: for a, b, c being Element of AFP holds
( not LIN a,b,c or not a <> b or not a <> c or not b <> c ) ; :: thesis: q,b // q9,y
A40: now :: thesis: ( q = p9 & p = q9 implies q,b // q9,y )
assume that
A41: q = p9 and
A42: p = q9 ; :: thesis: q,b // q9,y
A43: now :: thesis: ( b = x implies q,b // q9,y )
assume A44: b = x ; :: thesis: q,b // q9,y
then q,y // q,a by A14, A15, A27, A41, A42, AFF_1:5;
then LIN q,y,a by AFF_1:def 1;
then LIN a,y,q by AFF_1:6;
then q9,y // q,b by A7, A10, A13, A17, A29, A41, A42, A44, AFF_1:25;
hence q,b // q9,y by AFF_1:4; :: thesis: verum
end;
now :: thesis: not a = x
assume a = x ; :: thesis: contradiction
then a,p // a,q by A13, A41, AFF_1:4;
then LIN a,p,q by AFF_1:def 1;
then LIN p,q,a by AFF_1:6;
hence contradiction by A2, A3, A12, A16, A26, AFF_1:25; :: thesis: verum
end;
hence q,b // q9,y by A11, A31, A39, A43; :: thesis: verum
end;
now :: thesis: ( p = p9 & q = q9 implies q,b // q9,y )
assume that
A45: p = p9 and
A46: q = q9 ; :: thesis: q,b // q9,y
LIN p,b,y by A14, A45, AFF_1:def 1;
then LIN b,y,p by AFF_1:6;
then b = y by A8, A10, A17, A30, AFF_1:25;
hence q,b // q9,y by A46, AFF_1:2; :: thesis: verum
end;
hence q,b // q9,y by A12, A23, A22, A39, A36, A33, A40; :: thesis: verum
end;
A47: y in Line (p9,y) by AFF_1:15;
A48: p9 in Line (p9,y) by AFF_1:15;
A49: b in Line (p,b) by AFF_1:15;
then A50: Line (p,b) <> K by A1, A8, A24, AFF_1:45;
a <> q by A1, A3, A7, A24, AFF_1:45;
then A51: Line (q,a) // Line (q9,x) by A15, A25, AFF_1:37;
A52: p in Line (p,b) by AFF_1:15;
then A53: Line (p,b) <> M by A1, A2, A24, AFF_1:45;
A54: p9 <> y by A1, A4, A10, A24, AFF_1:45;
then A55: Line (p,b) // Line (p9,y) by A14, A27, AFF_1:37;
A56: Line (p9,y) is being_line by A54, AFF_1:def 3;
now :: thesis: ( ex a, b, c being Element of AFP st
( LIN a,b,c & a <> b & a <> c & b <> c ) implies q,b // q9,y )
A57: a,q // x,q9 by A18, A19, A21, A20, A51, AFF_1:39;
assume ex a, b, c being Element of AFP st
( LIN a,b,c & a <> b & a <> c & b <> c ) ; :: thesis: q,b // q9,y
then consider d being Element of AFP such that
A58: LIN p,b,d and
A59: d <> p and
A60: d <> b by TRANSLAC:1;
consider N being Subset of AFP such that
A61: d in N and
A62: K // N by A16, AFF_1:49;
A63: d in Line (p,b) by A58, AFF_1:def 2;
then A64: N <> M by A8, A17, A28, A49, A53, A60, A61, AFF_1:18;
A65: not Line (p9,y) // N
proof
assume Line (p9,y) // N ; :: thesis: contradiction
then Line (p,b) // N by A55, AFF_1:44;
then Line (p,b) // K by A62, AFF_1:44;
hence contradiction by A2, A52, A50, AFF_1:45; :: thesis: verum
end;
N is being_line by A62, AFF_1:36;
then consider z being Element of AFP such that
A66: z in Line (p9,y) and
A67: z in N by A56, A65, AFF_1:58;
A68: d,b // z,y by A49, A47, A55, A63, A66, AFF_1:39;
A69: N <> K by A2, A16, A28, A52, A50, A59, A63, A61, AFF_1:18;
A70: M // N by A1, A62, AFF_1:44;
A71: K <> N by A2, A16, A28, A52, A50, A59, A63, A61, AFF_1:18;
A72: N // M by A1, A62, AFF_1:44;
p,d // p9,z by A52, A48, A55, A63, A66, AFF_1:39;
then A73: a,d // x,z by A1, A2, A4, A6, A7, A9, A13, A24, A61, A62, A67, A71, Lm4;
M <> N by A8, A17, A28, A49, A53, A60, A63, A61, AFF_1:18;
then d,q // z,q9 by A1, A3, A5, A6, A7, A9, A24, A61, A67, A73, A57, A70, Lm4;
hence q,b // q9,y by A3, A5, A6, A8, A10, A61, A62, A67, A68, A72, A64, A69, Lm4; :: thesis: verum
end;
hence q,b // q9,y by A32; :: thesis: verum
end;
hence q,b // q9,y by A1, A3, A5, A8, A10, AFF_1:39; :: thesis: verum