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

proof

assume A1: AFP is translational ; :: thesis: for a, a', b, c, b', c' being Element of AFP st not LIN a,a',b & not LIN a,a',c & a,a' // b,b' & a,a' // c,c' & a,b // a',b' & a,c // a',c' holds
b,c // b',c'
let a, a', b, c, b', c' be Element of AFP; :: thesis: ( not LIN a,a',b & not LIN a,a',c & a,a' // b,b' & a,a' // c,c' & a,b // a',b' & a,c // a',c' implies b,c // b',c' )
assume A2: ( not LIN a,a',b & not LIN a,a',c & a,a' // b,b' & a,a' // c,c' & a,b // a',b' & a,c // a',c' ) ; :: thesis: b,c // b',c'
set A = Line a,a';
set P = Line b,b';
set C = Line c,c';
A3: ( a <> a' & a <> b & a' <> b & a <> c & a' <> c ) by A2, AFF_1:16;
A4: b <> b'

proof

assume b = b' ; :: thesis: contradiction
then b,a // b,a' by A2, AFF_1:13;
then LIN b,a,a' by AFF_1:def 1;
hence contradiction by A2, AFF_1:15; :: thesis: verum

end;

A5: c <> c'

proof

assume c = c' ; :: thesis: contradiction
then c,a // c,a' by A2, AFF_1:13;
then LIN c,a,a' by AFF_1:def 1;
hence contradiction by A2, AFF_1:15; :: thesis: verum

end;

A6: ( a in Line a,a' & a' in Line a,a' & b in Line b,b' & b' in Line b,b' & c in Line c,c' & c' in Line c,c' ) by AFF_1:26;
A7: ( Line a,a' is being_line & Line b,b' is being_line & Line c,c' is being_line ) by A3, A4, A5, AFF_1:def 3;
A8: ( Line a,a' // Line b,b' & Line a,a' // Line c,c' ) by A2, A3, A4, A5, AFF_1:51;
A9: Line a,a' <> Line b,b' by A2, A6, A7, AFF_1:33;
Line a,a' <> Line c,c' by A2, A6, A7, AFF_1:33;
hence b,c // b',c' by A1, A2, A6, A7, A8, A9, AFF_2:def 11; :: thesis: verum

end;

assume A10: for a, a', b, c, b', c' being Element of AFP st not LIN a,a',b & not LIN a,a',c & a,a' // b,b' & a,a' // c,c' & a,b // a',b' & a,c // a',c' holds
b,c // b',c' ; :: thesis: AFP is translational

now

let A, P, C be Subset of AFP; :: thesis: for a, b, c, a', b', c' being Element of AFP st A // P & A // C & a in A & a' in A & b in P & b' in P & c in C & c' in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a',b' & a,c // a',c' holds
b,c // b',c'
let a, b, c, a', b', c' be Element of AFP; :: thesis: ( A // P & A // C & a in A & a' in A & b in P & b' in P & c in C & c' in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a',b' & a,c // a',c' implies b,c // b',c' )
assume A11: ( A // P & A // C & a in A & a' in A & b in P & b' in P & c in C & c' in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a',b' & a,c // a',c' ) ; :: thesis: b,c // b',c'
then A12: ( a,a' // b,b' & a,a' // c,c' ) by AFF_1:53;

A13: now

assume A14: a = a' ; :: thesis: b,c // b',c'
then LIN a,b,b' by A11, AFF_1:def 1;
then LIN b,b',a by AFF_1:15;
then A15: ( b = b' or a in P ) by A11, AFF_1:39;
LIN a,c,c' by A11, A14, AFF_1:def 1;
then LIN c,c',a by AFF_1:15;
then ( c = c' or a in C ) by A11, AFF_1:39;
hence b,c // b',c' by A11, A15, AFF_1:11, AFF_1:59; :: thesis: verum

end;

now

assume A16: a <> a' ; :: thesis: b,c // b',c'
A17: not LIN a,a',b

proof

assume LIN a,a',b ; :: thesis: contradiction
then b in A by A11, A16, AFF_1:39;
hence contradiction by A11, AFF_1:59; :: thesis: verum

end;

not LIN a,a',c

proof

assume LIN a,a',c ; :: thesis: contradiction
then c in A by A11, A16, AFF_1:39;
hence contradiction by A11, AFF_1:59; :: thesis: verum

end;

hence b,c // b',c' by A10, A11, A12, A17; :: thesis: verum

end;

hence b,c // b',c' by A13; :: thesis: verum

end;

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