let AFP be AffinPlane; :: thesis: for a, b, x, p, q, p', q', y, y' being Element of AFP st AFP is translational & a <> b & LIN a,b,x & a,b // p,q & a,b // p',q' & a,p // b,q & a,p' // b,q' & p,q // x,y & p',q' // x,y' & p,x // q,y & p',x // q',y' & not LIN a,b,p & not LIN a,b,p' holds
y = y'
let a, b, x, p, q, p', q', y, y' be Element of AFP; :: thesis: ( AFP is translational & a <> b & LIN a,b,x & a,b // p,q & a,b // p',q' & a,p // b,q & a,p' // b,q' & p,q // x,y & p',q' // x,y' & p,x // q,y & p',x // q',y' & not LIN a,b,p & not LIN a,b,p' implies y = y' )
assume A1: ( AFP is translational & a <> b & LIN a,b,x & a,b // p,q & a,b // p',q' & a,p // b,q & a,p' // b,q' & p,q // x,y & p',q' // x,y' & p,x // q,y & p',x // q',y' & not LIN a,b,p & not LIN a,b,p' ) ; :: thesis: y = y'
then A2: ( a <> p & a <> p' ) by AFF_1:16;
A3: p <> q
proof
assume p = q ; :: thesis: contradiction
then p,a // p,b by A1, AFF_1:13;
then LIN p,a,b by AFF_1:def 1;
hence contradiction by A1, AFF_1:15; :: thesis: verum
end;
A4: p' <> q'
proof
assume p' = q' ; :: thesis: contradiction
then p',a // p',b by A1, AFF_1:13;
then LIN p',a,b by AFF_1:def 1;
hence contradiction by A1, AFF_1:15; :: thesis: verum
end;
A5: not LIN p,q,x
proof
assume LIN p,q,x ; :: thesis: contradiction
then p,q // p,x by AFF_1:def 1;
then a,b // p,x by A1, A3, AFF_1:14;
then a,b // x,p by AFF_1:13;
hence contradiction by A1, AFF_1:18; :: thesis: verum
end;
A6: not LIN p',q',x
proof
assume LIN p',q',x ; :: thesis: contradiction
then p',q' // p',x by AFF_1:def 1;
then a,b // p',x by A1, A4, AFF_1:14;
then a,b // x,p' by AFF_1:13;
hence contradiction by A1, AFF_1:18; :: thesis: verum
end;
A7: ( x <> y & x <> y' )
proof
now
assume x = y ; :: thesis: contradiction
then x,p // x,q by A1, AFF_1:13;
then LIN x,p,q by AFF_1:def 1;
hence contradiction by A5, AFF_1:15; :: thesis: verum
end;
hence x <> y ; :: thesis: x <> y'
now
assume x = y' ; :: thesis: contradiction
then x,p' // x,q' by A1, AFF_1:13;
then LIN x,p',q' by AFF_1:def 1;
hence contradiction by A6, AFF_1:15; :: thesis: verum
end;
hence x <> y' ; :: thesis: verum
end;
A8: LIN a,b,y
proof
a,b // x,y by A1, A3, AFF_1:14;
hence LIN a,b,y by A1, AFF_1:18; :: thesis: verum
end;
A9: not LIN q,p,b
proof
assume A10: LIN q,p,b ; :: thesis: contradiction
q,p // b,a by A1, AFF_1:13;
then ( LIN q,p,a & LIN q,p,p ) by A3, A10, AFF_1:16, AFF_1:18;
hence contradiction by A1, A3, A10, AFF_1:17; :: thesis: verum
end;
now
assume A11: LIN p,q,p' ; :: thesis: y = y'
A12: LIN p,q,q'
proof
p,q // p',q' by A1, AFF_1:14;
hence LIN p,q,q' by A3, A11, AFF_1:18; :: thesis: verum
end;
A13: now
assume A14: for x being Element of AFP holds
( not LIN a,p,x or x = a or x = p ) ; :: thesis: y = y'
then A15: for p, q, r being Element of AFP st p <> q & LIN p,q,r & not r = p holds
r = q by A2, Th2;
A16: now
assume A17: p = p' ; :: thesis: y = y'
then q = q' by A2, A3, A4, A12, A14, Th2;
hence y = y' by A1, A5, A17, TRANSGEO:97; :: thesis: verum
end;
now
assume A18: q = p' ; :: thesis: y = y'
A19: now
assume A20: a = x ; :: thesis: y = y'
then A21: b = y by A1, A7, A8, A14, Th2;
a,q // b,p by A1, A15, Th8;
then A22: ( q,p // a,b & q,a // p,b ) by A1, AFF_1:13;
A23: ( q,p // a,y' & q,a // p,y' ) by A1, A3, A4, A12, A14, A18, A20, Th2;
not LIN q,p,a by A5, A20, AFF_1:15;
hence y = y' by A21, A22, A23, TRANSGEO:97; :: thesis: verum
end;
now
assume A24: b = x ; :: thesis: y = y'
then A25: a = y by A1, A2, A7, A8, A14, Th2;
( q,p // b,a & q,p // b,y' & q,b // p,a & q,b // p,y' ) by A1, A2, A3, A4, A12, A14, A18, A24, Th2, AFF_1:13;
hence y = y' by A9, A25, TRANSGEO:97; :: thesis: verum
end;
hence y = y' by A1, A2, A14, A19, Th2; :: thesis: verum
end;
hence y = y' by A2, A3, A11, A14, A16, Th2; :: thesis: verum
end;
now
given p'' being Element of AFP such that A26: ( LIN a,p,p'' & p'' <> a & p'' <> p ) ; :: thesis: y = y'
consider q'' being Element of AFP such that
A27: a,b // p'',q'' and
A28: a,p'' // b,q'' by DIRAF:47;
consider y'' being Element of AFP such that
A29: p'',q'' // x,y'' and
A30: p'',x // q'',y'' by DIRAF:47;
A31: not LIN p,q,p''
proof
assume LIN p,q,p'' ; :: thesis: contradiction
then ( LIN p,p'',p & LIN p,p'',q & LIN p,p'',a ) by A26, AFF_1:15, AFF_1:16;
then LIN p,q,a by A26, AFF_1:17;
hence contradiction by A1, Lm5; :: thesis: verum
end;
A32: not LIN p',q',p''
proof
assume A33: LIN p',q',p'' ; :: thesis: contradiction
p,q // p',q' by A1, AFF_1:14;
then LIN p,q,q' by A3, A11, AFF_1:18;
hence contradiction by A4, A11, A31, A33, AFF_1:20; :: thesis: verum
end;
not LIN a,b,p''
proof
assume LIN a,b,p'' ; :: thesis: contradiction
then ( LIN a,p'',a & LIN a,p'',b & LIN a,p'',p ) by A26, AFF_1:15, AFF_1:16;
hence contradiction by A1, A26, AFF_1:17; :: thesis: verum
end;
then ( y = y'' & y' = y'' ) by A1, A27, A28, A29, A30, A31, A32, Lm8;
hence y = y' ; :: thesis: verum
end;
hence y = y' by A13; :: thesis: verum
end;
hence y = y' by A1, Lm8; :: thesis: verum