let AFP be AffinPlane; for a, b, p, p9, q, q9, x, y, y9 being Element of AFP st AFP is translational & a <> b & LIN a,b,x & a,b // p,q & a,b // p9,q9 & a,p // b,q & a,p9 // b,q9 & p,q // x,y & p9,q9 // x,y9 & p,x // q,y & p9,x // q9,y9 & not LIN a,b,p & not LIN a,b,p9 holds
y = y9
let a, b, p, p9, q, q9, x, y, y9 be Element of AFP; ( AFP is translational & a <> b & LIN a,b,x & a,b // p,q & a,b // p9,q9 & a,p // b,q & a,p9 // b,q9 & p,q // x,y & p9,q9 // x,y9 & p,x // q,y & p9,x // q9,y9 & not LIN a,b,p & not LIN a,b,p9 implies y = y9 )
assume that
A1:
AFP is translational
and
A2:
a <> b
and
A3:
LIN a,b,x
and
A4:
a,b // p,q
and
A5:
a,b // p9,q9
and
A6:
a,p // b,q
and
A7:
a,p9 // b,q9
and
A8:
p,q // x,y
and
A9:
p9,q9 // x,y9
and
A10:
p,x // q,y
and
A11:
p9,x // q9,y9
and
A12:
not LIN a,b,p
and
A13:
not LIN a,b,p9
; y = y9
A14:
p <> q
then
a,b // x,y
by A4, A8, AFF_1:5;
then A15:
LIN a,b,y
by A2, A3, AFF_1:9;
A16:
not LIN p,q,x
proof
assume
LIN p,
q,
x
;
contradiction
then
p,
q // p,
x
by AFF_1:def 1;
then
a,
b // p,
x
by A4, A14, AFF_1:5;
then
a,
b // x,
p
by AFF_1:4;
hence
contradiction
by A2, A3, A12, AFF_1:9;
verum
end;
A18:
p9 <> q9
A19:
not LIN q,p,b
proof
A20:
LIN q,
p,
p
by AFF_1:7;
assume A21:
LIN q,
p,
b
;
contradiction
q,
p // b,
a
by A4, AFF_1:4;
then
LIN q,
p,
a
by A14, A21, AFF_1:9;
hence
contradiction
by A12, A14, A21, A20, AFF_1:8;
verum
end;
now ( LIN p,q,p9 implies y = y9 )assume A22:
LIN p,
q,
p9
;
y = y9
p,
q // p9,
q9
by A2, A4, A5, AFF_1:5;
then A23:
LIN p,
q,
q9
by A14, A22, AFF_1:9;
A24:
now ( ( for x being Element of AFP holds
( not LIN a,p,x or x = a or x = p ) ) implies y = y9 )assume A25:
for
x being
Element of
AFP holds
( not
LIN a,
p,
x or
x = a or
x = p )
;
y = y9then A26:
for
p,
q,
r being
Element of
AFP st
p <> q &
LIN p,
q,
r & not
r = p holds
r = q
by Th1;
A27:
now ( q = p9 implies y = y9 )assume A28:
q = p9
;
y = y9A29:
now ( a = x implies y = y9 )
a,
q // b,
p
by A4, A6, A12, A26, Th6;
then A30:
q,
a // p,
b
by AFF_1:4;
A31:
q,
p // a,
b
by A4, AFF_1:4;
assume A32:
a = x
;
y = y9then A33:
(
q,
a // p,
y9 & not
LIN q,
p,
a )
by A11, A14, A18, A16, A23, A25, A28, Th1, AFF_1:6;
(
b = y &
q,
p // a,
y9 )
by A2, A9, A14, A18, A17, A15, A23, A25, A28, A32, Th1;
hence
y = y9
by A31, A30, A33, TRANSGEO:80;
verum end; now ( b = x implies y = y9 )A34:
(
q,
p // b,
a &
q,
b // p,
a )
by A4, A6, AFF_1:4;
assume A35:
b = x
;
y = y9then A36:
q,
b // p,
y9
by A11, A14, A18, A23, A25, A28, Th1;
(
a = y &
q,
p // b,
y9 )
by A2, A9, A14, A18, A17, A15, A23, A25, A28, A35, Th1;
hence
y = y9
by A19, A34, A36, TRANSGEO:80;
verum end; hence
y = y9
by A2, A3, A25, A29, Th1;
verum end; now ( p = p9 implies y = y9 )assume A37:
p = p9
;
y = y9then
q = q9
by A14, A18, A23, A25, Th1;
hence
y = y9
by A8, A9, A10, A11, A16, A37, TRANSGEO:80;
verum end; hence
y = y9
by A14, A22, A25, A27, Th1;
verum end; now ( ex p99 being Element of AFP st
( LIN a,p,p99 & p99 <> a & p99 <> p ) implies y = y9 )given p99 being
Element of
AFP such that A38:
LIN a,
p,
p99
and A39:
p99 <> a
and A40:
p99 <> p
;
y = y9A41:
not
LIN p,
q,
p99
proof
assume
LIN p,
q,
p99
;
contradiction
then A42:
LIN p,
p99,
q
by AFF_1:6;
(
LIN p,
p99,
p &
LIN p,
p99,
a )
by A38, AFF_1:6, AFF_1:7;
then
LIN p,
q,
a
by A40, A42, AFF_1:8;
hence
contradiction
by A4, A6, A12, Lm5;
verum
end; A43:
not
LIN p9,
q9,
p99
proof
p,
q // p9,
q9
by A2, A4, A5, AFF_1:5;
then A44:
LIN p,
q,
q9
by A14, A22, AFF_1:9;
assume
LIN p9,
q9,
p99
;
contradiction
hence
contradiction
by A18, A22, A41, A44, AFF_1:11;
verum
end; consider q99 being
Element of
AFP such that A45:
(
a,
b // p99,
q99 &
a,
p99 // b,
q99 )
by DIRAF:40;
consider y99 being
Element of
AFP such that A46:
(
p99,
q99 // x,
y99 &
p99,
x // q99,
y99 )
by DIRAF:40;
A47:
not
LIN a,
b,
p99
proof
assume
LIN a,
b,
p99
;
contradiction
then A48:
LIN a,
p99,
b
by AFF_1:6;
(
LIN a,
p99,
a &
LIN a,
p99,
p )
by A38, AFF_1:6, AFF_1:7;
hence
contradiction
by A12, A39, A48, AFF_1:8;
verum
end; then
y = y99
by A1, A2, A3, A4, A6, A8, A10, A12, A45, A46, A41, Lm8;
hence
y = y9
by A1, A2, A3, A5, A7, A9, A11, A13, A45, A46, A43, A47, Lm8;
verum end; hence
y = y9
by A24;
verum end;
hence
y = y9
by A1, A2, A3, A4, A5, A6, A7, A8, A9, A10, A11, A12, A13, Lm8; verum