let AFP be AffinPlane; :: thesis: for p, q, p', q', a, b, x, y being Element of
for K, M being Subset of st K // M & p in K & q in K & p' in K & q' in K & AFP is Moufangian & a in M & b in M & x in M & y in M & a <> b & q <> p & p,a // p',x & p,b // p',y & q,a // q',x holds
q,b // q',y
let p, q, p', q', a, b, x, y be Element of ; :: thesis: for K, M being Subset of st K // M & p in K & q in K & p' in K & q' in K & AFP is Moufangian & a in M & b in M & x in M & y in M & a <> b & q <> p & p,a // p',x & p,b // p',y & q,a // q',x holds
q,b // q',y
let K, M be Subset of ; :: thesis: ( K // M & p in K & q in K & p' in K & q' in K & AFP is Moufangian & a in M & b in M & x in M & y in M & a <> b & q <> p & p,a // p',x & p,b // p',y & q,a // q',x implies q,b // q',y )
assume that
A1: K // M and
A2: p in K and
A3: q in K and
A4: p' in K and
A5: q' 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 // p',x and
A14: p,b // p',y and
A15: q,a // q',x ; :: thesis: q,b // q',y
A16: K is being_line by A1, AFF_1:50;
A17: M is being_line by A1, AFF_1:50;
now
set D' = Line q',x;
set C' = Line q',y;
set B'' = Line p',y;
set A' = Line p',x;
set D = Line q,a;
set C = Line q,b;
set B' = 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 q',x by AFF_1:26;
A21: q' in Line q',x by AFF_1:26;
A22: LIN p,q,q' by A2, A3, A5, A16, AFF_1:33;
A23: LIN p,q,p' by A2, A3, A4, A16, AFF_1:33;
assume A24: K <> M ; :: thesis: q,b // q',y
then A25: q' <> 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 = p' and
A35: q = q' ; :: 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 = p' and
A38: p = q' ; :: 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,q' by A15, AFF_1:13;
then LIN a,q,q' 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 holds
( not LIN a,b,c or not a <> b or not a <> c or not b <> c ) ; :: thesis: q,b // q',y
A40: now
assume that
A41: q = p' and
A42: p = q' ; :: thesis: q,b // q',y
A43: now
assume A44: b = x ; :: thesis: q,b // q',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 q',y // q,b by A7, A10, A13, A17, A29, A41, A42, A44, AFF_1:39;
hence q,b // q',y by AFF_1:13; :: thesis: verum
end;
hence q,b // q',y by A11, A31, A39, A43; :: thesis: verum
end;
now
assume that
A45: p = p' and
A46: q = q' ; :: thesis: q,b // q',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 // q',y by A46, AFF_1:11; :: thesis: verum
end;
hence q,b // q',y by A12, A23, A22, A39, A36, A33, A40; :: thesis: verum
end;
A47: y in Line p',y by AFF_1:26;
A48: p' in Line p',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 q',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: p' <> y by A1, A4, A10, A24, AFF_1:59;
then A55: Line p,b // Line p',y by A14, A27, AFF_1:51;
A56: Line p',y is being_line by A54, AFF_1:def 3;
now
A57: a,q // x,q' by A18, A19, A21, A20, A51, AFF_1:53;
assume ex a, b, c being Element of st
( LIN a,b,c & a <> b & a <> c & b <> c ) ; :: thesis: q,b // q',y
then consider d being Element of such that
A58: LIN p,b,d and
A59: d <> p and
A60: d <> b by TRANSLAC:2;
consider N being Subset of 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 p',y // N
proof
assume Line p',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 such that
A66: z in Line p',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 // p',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,q' by A1, A3, A5, A6, A7, A9, A24, A61, A67, A73, A57, A70, Lm4;
hence q,b // q',y by A3, A5, A6, A8, A10, A61, A62, A67, A68, A72, A64, A69, Lm4; :: thesis: verum
end;
hence q,b // q',y by A32; :: thesis: verum
end;
hence q,b // q',y by A1, A3, A5, A8, A10, AFF_1:53; :: thesis: verum