let AFP be AffinPlane; :: thesis: ( AFP is translational iff for a, a9, b, c, b9, c9 being Element of AFP st not LIN a,a9,b & not LIN a,a9,c & a,a9 // b,b9 & a,a9 // c,c9 & a,b // a9,b9 & a,c // a9,c9 holds
b,c // b9,c9 )
thus ( AFP is translational implies for a, a9, b, c, b9, c9 being Element of AFP st not LIN a,a9,b & not LIN a,a9,c & a,a9 // b,b9 & a,a9 // c,c9 & a,b // a9,b9 & a,c // a9,c9 holds
b,c // b9,c9 ) :: thesis: ( ( for a, a9, b, c, b9, c9 being Element of AFP st not LIN a,a9,b & not LIN a,a9,c & a,a9 // b,b9 & a,a9 // c,c9 & a,b // a9,b9 & a,c // a9,c9 holds
b,c // b9,c9 ) implies AFP is translational )

proof

assume A1: AFP is translational ; :: thesis: for a, a9, b, c, b9, c9 being Element of AFP st not LIN a,a9,b & not LIN a,a9,c & a,a9 // b,b9 & a,a9 // c,c9 & a,b // a9,b9 & a,c // a9,c9 holds
b,c // b9,c9
let a, a9, b, c, b9, c9 be Element of AFP; :: thesis: ( not LIN a,a9,b & not LIN a,a9,c & a,a9 // b,b9 & a,a9 // c,c9 & a,b // a9,b9 & a,c // a9,c9 implies b,c // b9,c9 )
assume that
A2: not LIN a,a9,b and
A3: not LIN a,a9,c and
A4: a,a9 // b,b9 and
A5: a,a9 // c,c9 and
A6: a,b // a9,b9 and
A7: a,c // a9,c9 ; :: thesis: b,c // b9,c9
set A = Line (a,a9);
set P = Line (b,b9);
set C = Line (c,c9);
A8: ( a in Line (a,a9) & a9 in Line (a,a9) ) by AFF_1:15;
A9: c <> c9

proof

assume c = c9 ; :: thesis: contradiction
then c,a // c,a9 by A7, AFF_1:4;
then LIN c,a,a9 by AFF_1:def 1;
hence contradiction by A3, AFF_1:6; :: thesis: verum

end;

then A10: Line (c,c9) is being_line by AFF_1:def 3;
A11: b <> b9

proof

assume b = b9 ; :: thesis: contradiction
then b,a // b,a9 by A6, AFF_1:4;
then LIN b,a,a9 by AFF_1:def 1;
hence contradiction by A2, AFF_1:6; :: thesis: verum

end;

then A12: Line (b,b9) is being_line by AFF_1:def 3;
A13: a <> a9 by A2, AFF_1:7;
then A14: Line (a,a9) is being_line by AFF_1:def 3;
A15: c in Line (c,c9) by AFF_1:15;
then A16: Line (a,a9) <> Line (c,c9) by A3, A8, A14, AFF_1:21;
A17: Line (a,a9) // Line (b,b9) by A4, A13, A11, AFF_1:37;
A18: ( b9 in Line (b,b9) & c9 in Line (c,c9) ) by AFF_1:15;
A19: Line (a,a9) // Line (c,c9) by A5, A13, A9, AFF_1:37;
A20: b in Line (b,b9) by AFF_1:15;
then Line (a,a9) <> Line (b,b9) by A2, A8, A14, AFF_1:21;
hence b,c // b9,c9 by A1, A6, A7, A8, A20, A15, A18, A14, A12, A10, A17, A19, A16, AFF_2:def 11; :: thesis: verum

end;

assume A21: for a, a9, b, c, b9, c9 being Element of AFP st not LIN a,a9,b & not LIN a,a9,c & a,a9 // b,b9 & a,a9 // c,c9 & a,b // a9,b9 & a,c // a9,c9 holds
b,c // b9,c9 ; :: thesis: AFP is translational

now :: thesis: for A, P, C being Subset of AFP
for a, b, c, a9, b9, c9 being Element of AFP st A // P & A // C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 holds
b,c // b9,c9

let A, P, C be Subset of AFP; :: thesis: for a, b, c, a9, b9, c9 being Element of AFP st A // P & A // C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 holds
b,c // b9,c9
let a, b, c, a9, b9, c9 be Element of AFP; :: thesis: ( A // P & A // C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 implies b,c // b9,c9 )
assume that
A22: A // P and
A23: A // C and
A24: a in A and
A25: a9 in A and
A26: b in P and
A27: b9 in P and
A28: c in C and
A29: c9 in C and
A30: A is being_line and
A31: P is being_line and
A32: C is being_line and
A33: A <> P and
A34: A <> C and
A35: a,b // a9,b9 and
A36: a,c // a9,c9 ; :: thesis: b,c // b9,c9
A37: ( a,a9 // b,b9 & a,a9 // c,c9 ) by A22, A23, A24, A25, A26, A27, A28, A29, AFF_1:39;

A38: now :: thesis: ( a <> a9 implies b,c // b9,c9 )

assume A39: a <> a9 ; :: thesis: b,c // b9,c9
A40: not LIN a,a9,c

proof

assume LIN a,a9,c ; :: thesis: contradiction
then c in A by A24, A25, A30, A39, AFF_1:25;
hence contradiction by A23, A28, A34, AFF_1:45; :: thesis: verum

end;

not LIN a,a9,b

proof

assume LIN a,a9,b ; :: thesis: contradiction
then b in A by A24, A25, A30, A39, AFF_1:25;
hence contradiction by A22, A26, A33, AFF_1:45; :: thesis: verum

end;

hence b,c // b9,c9 by A21, A35, A36, A37, A40; :: thesis: verum

end;

now :: thesis: ( a = a9 implies b,c // b9,c9 )

assume A41: a = a9 ; :: thesis: b,c // b9,c9
then LIN a,c,c9 by A36, AFF_1:def 1;
then LIN c,c9,a by AFF_1:6;
then A42: ( c = c9 or a in C ) by A28, A29, A32, AFF_1:25;
LIN a,b,b9 by A35, A41, AFF_1:def 1;
then LIN b,b9,a by AFF_1:6;
then ( b = b9 or a in P ) by A26, A27, A31, AFF_1:25;
hence b,c // b9,c9 by A22, A23, A24, A33, A34, A42, AFF_1:2, AFF_1:45; :: thesis: verum

end;

hence b,c // b9,c9 by A38; :: thesis: verum

end;

hence AFP is translational by AFF_2:def 11; :: thesis: verum