let AFP be AffinPlane; :: thesis: for p, q, p9, q9, a, b, x, y being Element of AFP
for K, M 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 p, q, p9, q9, a, b, x, y be Element of AFP; :: thesis: for K, M 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 K, M 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:50;
A17: M is being_line by A1, AFF_1:50;
now
set D9 = Line q9,x;
set C9 = Line q9,y;
set B99 = Line p9,y;
set A9 = Line p9,x;
set D = Line q,a;
set C = Line q,b;
set B9 = Line p,b;
set A = Line p,a;
A18: q in Line q,a by AFF_1:26;
A19: a in Line q,a by AFF_1:26;
A20: x in Line q9,x by AFF_1:26;
A21: q9 in Line q9,x by AFF_1:26;
A22: LIN p,q,q9 by A2, A3, A5, A16, AFF_1:33;
A23: LIN p,q,p9 by A2, A3, A4, A16, AFF_1:33;
assume A24: K <> M ; :: thesis: q,b // q9,y
then A25: q9 <> x by A1, A5, A9, AFF_1:59;
A26: not a in K by A1, A7, A24, AFF_1:59;
A27: b <> p by A1, A2, A8, A24, AFF_1:59;
then A28: Line p,b is being_line by AFF_1:def 3;
A29: not q in M by A1, A3, A24, AFF_1:59;
A30: not p in M by A1, A2, A24, AFF_1:59;
A31: LIN a,b,x by A7, A8, A9, A17, AFF_1:33;
A32: now
A33: now
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:15;
then a = x by A7, A9, A17, A29, AFF_1:39;
then a,q // a,p by A13, A34, AFF_1:13;
then LIN a,q,p by AFF_1:def 1;
then LIN p,q,a by AFF_1:15;
hence contradiction by A2, A3, A12, A16, A26, AFF_1:39; :: thesis: verum
end;
A36: now
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:15;
then a = x by A7, A9, A17, A30, AFF_1:39;
then a,q // a,q9 by A15, AFF_1:13;
then LIN a,q,q9 by AFF_1:def 1;
then LIN p,q,a by A38, AFF_1:15;
hence contradiction by A2, A3, A12, A16, A26, AFF_1:39; :: 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
assume that
A41: q = p9 and
A42: p = q9 ; :: thesis: q,b // q9,y
A43: now
assume A44: b = x ; :: thesis: q,b // q9,y
then q,y // q,a by A14, A15, A27, A41, A42, AFF_1:14;
then LIN q,y,a by AFF_1:def 1;
then LIN a,y,q by AFF_1:15;
then q9,y // q,b by A7, A10, A13, A17, A29, A41, A42, A44, AFF_1:39;
hence q,b // q9,y by AFF_1:13; :: thesis: verum
end;
hence q,b // q9,y by A11, A31, A39, A43; :: thesis: verum
end;
now
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:15;
then b = y by A8, A10, A17, A30, AFF_1:39;
hence q,b // q9,y by A46, AFF_1:11; :: 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:26;
A48: p9 in Line p9,y by AFF_1:26;
A49: b in Line p,b by AFF_1:26;
then A50: Line p,b <> K by A1, A8, A24, AFF_1:59;
a <> q by A1, A3, A7, A24, AFF_1:59;
then A51: Line q,a // Line q9,x by A15, A25, AFF_1:51;
A52: p in Line p,b by AFF_1:26;
then A53: Line p,b <> M by A1, A2, A24, AFF_1:59;
A54: p9 <> y by A1, A4, A10, A24, AFF_1:59;
then A55: Line p,b // Line p9,y by A14, A27, AFF_1:51;
A56: Line p9,y is being_line by A54, AFF_1:def 3;
now
A57: a,q // x,q9 by A18, A19, A21, A20, A51, AFF_1:53;
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:2;
consider N being Subset of AFP such that
A61: d in N and
A62: K // N by A16, AFF_1:63;
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:30;
A65: not Line p9,y // N
proof
assume Line p9,y // N ; :: thesis: contradiction
then Line p,b // N by A55, AFF_1:58;
then Line p,b // K by A62, AFF_1:58;
hence contradiction by A2, A52, A50, AFF_1:59; :: thesis: verum
end;
N is being_line by A62, AFF_1:50;
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:72;
A68: d,b // z,y by A49, A47, A55, A63, A66, AFF_1:53;
A69: N <> K by A2, A16, A28, A52, A50, A59, A63, A61, AFF_1:30;
A70: M // N by A1, A62, AFF_1:58;
A71: K <> N by A2, A16, A28, A52, A50, A59, A63, A61, AFF_1:30;
A72: N // M by A1, A62, AFF_1:58;
p,d // p9,z by A52, A48, A55, A63, A66, AFF_1:53;
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:30;
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:53; :: thesis: verum