let AP be AffinPlane; :: thesis: ( AP is translational implies AP is satisfying_pap )
assume A1: AP is translational ; :: thesis: AP is satisfying_pap
thus AP is satisfying_pap :: thesis: verum

proof

let M be Subset of AP; :: according to AFF_2:def 13 :: thesis: for N being Subset of AP
for a, b, c, a9, b9, c9 being Element of AP st M is being_line & N is being_line & a in M & b in M & c in M & M // N & M <> N & a9 in N & b9 in N & c9 in N & a,b9 // b,a9 & b,c9 // c,b9 holds
a,c9 // c,a9
let N be Subset of AP; :: thesis: for a, b, c, a9, b9, c9 being Element of AP st M is being_line & N is being_line & a in M & b in M & c in M & M // N & M <> N & a9 in N & b9 in N & c9 in N & a,b9 // b,a9 & b,c9 // c,b9 holds
a,c9 // c,a9
let a, b, c, a9, b9, c9 be Element of AP; :: thesis: ( M is being_line & N is being_line & a in M & b in M & c in M & M // N & M <> N & a9 in N & b9 in N & c9 in N & a,b9 // b,a9 & b,c9 // c,b9 implies a,c9 // c,a9 )
assume that
A2: M is being_line and
A3: N is being_line and
A4: a in M and
A5: b in M and
A6: c in M and
A7: M // N and
A8: M <> N and
A9: a9 in N and
A10: b9 in N and
A11: c9 in N and
A12: a,b9 // b,a9 and
A13: b,c9 // c,b9 ; :: thesis: a,c9 // c,a9
set A = Line a,b9;
set A9 = Line b,a9;
set P = Line b,c9;
set P9 = Line c,b9;
A14: c <> b9 by A6, A7, A8, A10, AFF_1:59;
then A15: ( c in Line c,b9 & b9 in Line c,b9 ) by AFF_1:38;
A16: b <> c9 by A5, A7, A8, A11, AFF_1:59;
then A17: ( Line b,c9 is being_line & b in Line b,c9 ) by AFF_1:38;
A18: Line c,b9 is being_line by A14, AFF_1:38;
then consider C9 being Subset of AP such that
A19: a in C9 and
A20: Line c,b9 // C9 by AFF_1:63;
A21: C9 is being_line by A20, AFF_1:50;
assume A22: not a,c9 // c,a9 ; :: thesis: contradiction

A23: now

assume A24: a = c ; :: thesis: contradiction
then b,c9 // b,a9 by A12, A13, A14, AFF_1:14;
then LIN b,c9,a9 by AFF_1:def 1;
then LIN a9,c9,b by AFF_1:15;
then ( a9 = c9 or b in N ) by A3, A9, A11, AFF_1:39;
hence contradiction by A5, A7, A8, A22, A24, AFF_1:11, AFF_1:59; :: thesis: verum

end;

A25: Line c,b9 <> C9

proof

assume Line c,b9 = C9 ; :: thesis: contradiction
then LIN a,c,b9 by A18, A15, A19, AFF_1:33;
then b9 in M by A2, A4, A6, A23, AFF_1:39;
hence contradiction by A7, A8, A10, AFF_1:59; :: thesis: verum

end;

A26: c9 in Line b,c9 by A16, AFF_1:38;
then A27: Line c,b9 // Line b,c9 by A13, A16, A14, A18, A17, A15, AFF_1:52;

A28: now

assume A29: b = c ; :: thesis: contradiction
then LIN b,c9,b9 by A13, AFF_1:def 1;
then LIN b9,c9,b by AFF_1:15;
then ( b9 = c9 or b in N ) by A3, A10, A11, AFF_1:39;
hence contradiction by A5, A7, A8, A12, A22, A29, AFF_1:59; :: thesis: verum

end;

A30: Line c,b9 <> Line b,c9

proof

assume Line c,b9 = Line b,c9 ; :: thesis: contradiction
then LIN b,c,b9 by A17, A15, AFF_1:33;
then b9 in M by A2, A5, A6, A28, AFF_1:39;
hence contradiction by A7, A8, A10, AFF_1:59; :: thesis: verum

end;

A31: a <> b9 by A4, A7, A8, A10, AFF_1:59;
then A32: Line a,b9 is being_line by AFF_1:38;
then consider C being Subset of AP such that
A33: c in C and
A34: Line a,b9 // C by AFF_1:63;
A35: C is being_line by A34, AFF_1:50;
A36: a,b // b9,a9 by A4, A5, A7, A9, A10, AFF_1:53;
A37: b9,c9 // c,b by A5, A6, A7, A10, A11, AFF_1:53;
A38: b <> a9 by A5, A7, A8, A9, AFF_1:59;
then A39: a9 in Line b,a9 by AFF_1:38;
A40: ( a in Line a,b9 & b9 in Line a,b9 ) by A31, AFF_1:38;
A41: Line a,b9 <> C

proof

assume Line a,b9 = C ; :: thesis: contradiction
then LIN a,c,b9 by A32, A40, A33, AFF_1:33;
then b9 in M by A2, A4, A6, A23, AFF_1:39;
hence contradiction by A7, A8, A10, AFF_1:59; :: thesis: verum

end;

not C // C9

proof

assume C // C9 ; :: thesis: contradiction
then Line a,b9 // C9 by A34, AFF_1:58;
then Line a,b9 // Line c,b9 by A20, AFF_1:58;
then b9,a // b9,c by A40, A15, AFF_1:53;
then LIN b9,a,c by AFF_1:def 1;
then LIN a,c,b9 by AFF_1:15;
then b9 in M by A2, A4, A6, A23, AFF_1:39;
hence contradiction by A7, A8, A10, AFF_1:59; :: thesis: verum

end;

then consider s being Element of AP such that
A42: s in C and
A43: s in C9 by A35, A21, AFF_1:72;
A44: ( Line b,a9 is being_line & b in Line b,a9 ) by A38, AFF_1:38;

A45: now

assume A46: a = b ; :: thesis: contradiction
then LIN a,b9,a9 by A12, AFF_1:def 1;
then LIN a9,b9,a by AFF_1:15;
then ( a9 = b9 or a in N ) by A3, A9, A10, AFF_1:39;
hence contradiction by A4, A7, A8, A13, A22, A46, AFF_1:59; :: thesis: verum

end;

A47: now

assume a9 = b9 ; :: thesis: contradiction
then a9,a // a9,b by A12, AFF_1:13;
then LIN a9,a,b by AFF_1:def 1;
then LIN a,b,a9 by AFF_1:15;
then a9 in M by A2, A4, A5, A45, AFF_1:39;
hence contradiction by A7, A8, A9, AFF_1:59; :: thesis: verum

end;

A48: Line a,b9 <> Line b,a9

proof

assume Line a,b9 = Line b,a9 ; :: thesis: contradiction
then LIN a9,b9,a by A32, A40, A39, AFF_1:33;
then a in N by A3, A9, A10, A47, AFF_1:39;
hence contradiction by A4, A7, A8, AFF_1:59; :: thesis: verum

end;

A49: b <> s

proof

assume b = s ; :: thesis: contradiction
then a,b9 // b,c by A40, A33, A34, A42, AFF_1:53;
then b,a9 // b,c by A12, A31, AFF_1:14;
then LIN b,a9,c by AFF_1:def 1;
then LIN b,c,a9 by AFF_1:15;
then a9 in M by A2, A5, A6, A28, AFF_1:39;
hence contradiction by A7, A8, A9, AFF_1:59; :: thesis: verum

end;

A50: Line a,b9 // Line b,a9 by A12, A31, A38, AFF_1:51;
a,s // b9,c by A15, A19, A20, A43, AFF_1:53;
then A51: b,s // a9,c by A1, A32, A40, A44, A39, A33, A34, A35, A42, A36, A48, A41, A50, Def11;
b9,a // c,s by A40, A33, A34, A42, AFF_1:53;
then c9,a // b,s by A1, A18, A17, A26, A15, A19, A20, A21, A43, A37, A30, A25, A27, Def11;
then c9,a // a9,c by A51, A49, AFF_1:14;
hence contradiction by A22, AFF_1:13; :: thesis: verum

end;