let AFP be AffinPlane; :: thesis: for a, b, o, r, x, y being Element of AFP st o <> a & LIN o,a,b & AFP is Desarguesian & LIN o,a,x & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,r & LIN o,a,r ) holds
y = r
let a, b, o, r, x, y be Element of AFP; :: thesis: ( o <> a & LIN o,a,b & AFP is Desarguesian & LIN o,a,x & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,r & LIN o,a,r ) implies y = r )
assume that
A1: o <> a and
A2: LIN o,a,b and
A3: AFP is Desarguesian and
A4: LIN o,a,x and
A5: ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) and
A6: ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,r & LIN o,a,r ) ; :: thesis: y = r
consider q, q9 being Element of AFP such that
A7: not LIN o,a,q and
A8: LIN o,q,q9 and
A9: a,q // b,q9 and
A10: q,x // q9,r and
A11: LIN o,a,r by A6;
A12: o <> q by A7, AFF_1:7;
consider p, p9 being Element of AFP such that
A13: not LIN o,a,p and
A14: LIN o,p,p9 and
A15: a,p // b,p9 and
A16: p,x // p9,y and
A17: LIN o,a,y by A5;
A18: ( a = x implies y = r )
proof
A19: q,a // q9,b by A9, AFF_1:4;
A20: not LIN o,q,a by A7, AFF_1:6;
A21: p,a // p9,b by A15, AFF_1:4;
assume A22: a = x ; :: thesis: y = r
not LIN o,p,a by A13, AFF_1:6;
then b = y by A2, A14, A16, A17, A22, A21, AFF_1:56;
hence y = r by A2, A8, A10, A11, A22, A20, A19, AFF_1:56; :: thesis: verum
end;
A23: o <> p by A13, AFF_1:7;
A24: ( a <> b & a <> x & p <> q & o <> x implies y = r )
proof
assume that
a <> b and
a <> x and
A25: p <> q and
A26: o <> x ; :: thesis: y = r
A27: now :: thesis: ( LIN o,p,q implies y = r )
set K = Line (o,p);
set A = Line (o,a);
A28: LIN o,q,o by AFF_1:7;
A29: o in Line (o,a) by AFF_1:15;
A30: p in Line (o,p) by AFF_1:15;
A31: o in Line (o,p) by AFF_1:15;
A32: Line (o,a) is being_line by A1, AFF_1:def 3;
A33: x in Line (o,a) by A4, AFF_1:def 2;
r in Line (o,a) by A11, AFF_1:def 2;
then A34: LIN o,x,r by A32, A29, A33, AFF_1:21;
A35: x,p // y,p9 by A16, AFF_1:4;
assume A36: LIN o,p,q ; :: thesis: y = r
then LIN o,q,p by AFF_1:6;
then LIN o,p,q9 by A8, A12, A28, AFF_1:8;
then x,q // y,q9 by A2, A3, A4, A13, A14, A15, A17, A9, A12, A25, A26, A36, A35, Th1;
then A37: q,x // q9,y by AFF_1:4;
A38: Line (o,p) is being_line by A23, AFF_1:def 3;
A39: q in Line (o,p) by A36, AFF_1:def 2;
A40: not LIN o,q,x
proof
assume A41: LIN o,q,x ; :: thesis: contradiction
Line (o,p) = Line (o,q) by A12, A38, A31, A39, AFF_1:24;
then x in Line (o,p) by A41, AFF_1:def 2;
then A42: p in Line (o,a) by A26, A32, A29, A33, A38, A31, A30, AFF_1:18;
A43: a in Line (o,a) by AFF_1:15;
Line (o,a) is being_line by A1, AFF_1:def 3;
hence contradiction by A13, A29, A43, A42, AFF_1:21; :: thesis: verum
end;
y in Line (o,a) by A17, AFF_1:def 2;
then LIN o,x,y by A32, A29, A33, AFF_1:21;
hence y = r by A8, A10, A37, A40, A34, AFF_1:56; :: thesis: verum
end;
now :: thesis: ( not LIN o,p,q implies y = r )
A44: not LIN o,p,x
proof
assume LIN o,p,x ; :: thesis: contradiction
then A45: LIN o,x,p by AFF_1:6;
LIN o,a,o by AFF_1:7;
hence contradiction by A4, A13, A26, A45, AFF_1:11; :: thesis: verum
end;
set K = Line (o,q);
set A = Line (o,a);
assume A46: not LIN o,p,q ; :: thesis: y = r
A47: o in Line (o,a) by AFF_1:15;
A48: q in Line (o,q) by AFF_1:15;
A49: o in Line (o,q) by AFF_1:15;
A50: Line (o,a) is being_line by A1, AFF_1:def 3;
A51: x in Line (o,a) by A4, AFF_1:def 2;
A52: y in Line (o,a) by A17, AFF_1:def 2;
then A53: LIN o,x,y by A50, A47, A51, AFF_1:21;
A54: Line (o,q) is being_line by A12, AFF_1:def 3;
A55: not LIN o,q,x r in Line (o,a) by A11, AFF_1:def 2;
then A58: LIN o,x,r by A50, A47, A51, AFF_1:21;
A59: LIN o,x,y by A50, A47, A51, A52, AFF_1:21;
p,q // p9,q9 by A2, A3, A13, A14, A15, A7, A8, A9, Lm1;
then q,x // q9,y by A3, A14, A16, A8, A46, A44, A53, Lm1;
hence y = r by A8, A10, A55, A59, A58, AFF_1:56; :: thesis: verum
end;
hence y = r by A27; :: thesis: verum
end;
A60: o <> a by A13, AFF_1:7;
A61: ( p = q & o <> x implies y = r )
proof
assume that
A62: p = q and
A63: o <> x ; :: thesis: y = r
A64: not LIN o,p,x
proof
assume LIN o,p,x ; :: thesis: contradiction
then A65: LIN o,x,p by AFF_1:6;
A66: LIN o,x,o by AFF_1:7;
LIN o,x,a by A4, AFF_1:6;
hence contradiction by A13, A63, A66, A65, AFF_1:8; :: thesis: verum
end;
A67: LIN o,a,o by AFF_1:7;
then A68: LIN o,x,y by A4, A17, A60, AFF_1:8;
A69: LIN o,x,r by A4, A11, A60, A67, AFF_1:8;
p9 = q9 by A2, A13, A14, A15, A8, A9, A62, AFF_1:56;
hence y = r by A14, A16, A10, A62, A68, A69, A64, AFF_1:56; :: thesis: verum
end;
A70: ( o = x implies y = r )
proof
assume A71: o = x ; :: thesis: y = r
then y = o by A1, A4, A5, Lm7;
hence y = r by A1, A4, A6, A71, Lm7; :: thesis: verum
end;
( a = b implies y = r )
proof
assume A72: a = b ; :: thesis: y = r
then x = y by A1, A4, A5, Lm10;
hence y = r by A1, A4, A6, A72, Lm10; :: thesis: verum
end;
hence y = r by A70, A61, A18, A24; :: thesis: verum