let AFP be AffinPlane; :: thesis: ( AFP is translational iff for a, a', b, c, b', c' being Element of 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 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 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 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 ; :: 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 that
A2: not LIN a,a',b and
A3: not LIN a,a',c and
A4: a,a' // b,b' and
A5: a,a' // c,c' and
A6: a,b // a',b' and
A7: a,c // a',c' ; :: thesis: b,c // b',c'
set A = Line a,a';
set P = Line b,b';
set C = Line c,c';
A8: ( a in Line a,a' & a' in Line a,a' ) by AFF_1:26;
A9: c <> c'

proof

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

end;

then A10: Line c,c' is being_line by AFF_1:def 3;
A11: b <> b'

proof

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

end;

then A12: Line b,b' is being_line by AFF_1:def 3;
A13: a <> a' by A2, AFF_1:16;
then A14: Line a,a' is being_line by AFF_1:def 3;
A15: c in Line c,c' by AFF_1:26;
then A16: Line a,a' <> Line c,c' by A3, A8, A14, AFF_1:33;
A17: Line a,a' // Line b,b' by A4, A13, A11, AFF_1:51;
A18: ( b' in Line b,b' & c' in Line c,c' ) by AFF_1:26;
A19: Line a,a' // Line c,c' by A5, A13, A9, AFF_1:51;
A20: b in Line b,b' by AFF_1:26;
then Line a,a' <> Line b,b' by A2, A8, A14, AFF_1:33;
hence b,c // b',c' 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, a', b, c, b', c' being Element of 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 ; :: thesis: for a, b, c, a', b', c' being Element of 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 ; :: 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 that
A22: A // P and
A23: A // C and
A24: a in A and
A25: a' in A and
A26: b in P and
A27: b' in P and
A28: c in C and
A29: c' 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 // a',b' and
A36: a,c // a',c' ; :: thesis: b,c // b',c'
A37: ( a,a' // b,b' & a,a' // c,c' ) by A22, A23, A24, A25, A26, A27, A28, A29, AFF_1:53;

A38: now

assume A39: a <> a' ; :: thesis: b,c // b',c'
A40: not LIN a,a',c

proof

assume LIN a,a',c ; :: thesis: contradiction
then c in A by A24, A25, A30, A39, AFF_1:39;
hence contradiction by A23, A28, A34, AFF_1:59; :: thesis: verum

end;

not LIN a,a',b

proof

assume LIN a,a',b ; :: thesis: contradiction
then b in A by A24, A25, A30, A39, AFF_1:39;
hence contradiction by A22, A26, A33, AFF_1:59; :: thesis: verum

end;

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

end;

now

assume A41: a = a' ; :: thesis: b,c // b',c'
then LIN a,c,c' by A36, AFF_1:def 1;
then LIN c,c',a by AFF_1:15;
then A42: ( c = c' or a in C ) by A28, A29, A32, AFF_1:39;
LIN a,b,b' by A35, A41, AFF_1:def 1;
then LIN b,b',a by AFF_1:15;
then ( b = b' or a in P ) by A26, A27, A31, AFF_1:39;
hence b,c // b',c' by A22, A23, A24, A33, A34, A42, AFF_1:11, AFF_1:59; :: thesis: verum

end;

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

end;

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