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 ; :: according to AFF_2:def 13 :: thesis: for N being Subset of
for a, b, c, a', b', c' being Element of st M is being_line & N is being_line & a in M & b in M & c in M & M // N & M <> N & a' in N & b' in N & c' in N & a,b' // b,a' & b,c' // c,b' holds
a,c' // c,a'
let N be Subset of ; :: thesis: for a, b, c, a', b', c' being Element of st M is being_line & N is being_line & a in M & b in M & c in M & M // N & M <> N & a' in N & b' in N & c' in N & a,b' // b,a' & b,c' // c,b' holds
a,c' // c,a'
let a, b, c, a', b', c' be Element of ; :: thesis: ( M is being_line & N is being_line & a in M & b in M & c in M & M // N & M <> N & a' in N & b' in N & c' in N & a,b' // b,a' & b,c' // c,b' implies a,c' // c,a' )
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: a' in N and
A10: b' in N and
A11: c' in N and
A12: a,b' // b,a' and
A13: b,c' // c,b' ; :: thesis: a,c' // c,a'
set A = Line a,b';
set A' = Line b,a';
set P = Line b,c';
set P' = Line c,b';
A14: c <> b' by A6, A7, A8, A10, AFF_1:59;
then A15: ( c in Line c,b' & b' in Line c,b' ) by AFF_1:38;
A16: b <> c' by A5, A7, A8, A11, AFF_1:59;
then A17: ( Line b,c' is being_line & b in Line b,c' ) by AFF_1:38;
A18: Line c,b' is being_line by A14, AFF_1:38;
then consider C' being Subset of such that
A19: a in C' and
A20: Line c,b' // C' by AFF_1:63;
A21: C' is being_line by A20, AFF_1:50;
assume A22: not a,c' // c,a' ; :: thesis: contradiction

A23: now

assume A24: a = c ; :: thesis: contradiction
then b,c' // b,a' by A12, A13, A14, AFF_1:14;
then LIN b,c',a' by AFF_1:def 1;
then LIN a',c',b by AFF_1:15;
then ( a' = c' 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,b' <> C'

proof

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

end;

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

A28: now

assume A29: b = c ; :: thesis: contradiction
then LIN b,c',b' by A13, AFF_1:def 1;
then LIN b',c',b by AFF_1:15;
then ( b' = c' 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,b' <> Line b,c'

proof

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

end;

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

proof

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

end;

not C // C'

proof

assume C // C' ; :: thesis: contradiction
then Line a,b' // C' by A34, AFF_1:58;
then Line a,b' // Line c,b' by A20, AFF_1:58;
then b',a // b',c by A40, A15, AFF_1:53;
then LIN b',a,c by AFF_1:def 1;
then LIN a,c,b' by AFF_1:15;
then b' 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 such that
A42: s in C and
A43: s in C' by A35, A21, AFF_1:72;
A44: ( Line b,a' is being_line & b in Line b,a' ) by A38, AFF_1:38;

A45: now

assume A46: a = b ; :: thesis: contradiction
then LIN a,b',a' by A12, AFF_1:def 1;
then LIN a',b',a by AFF_1:15;
then ( a' = b' 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 a' = b' ; :: thesis: contradiction
then a',a // a',b by A12, AFF_1:13;
then LIN a',a,b by AFF_1:def 1;
then LIN a,b,a' by AFF_1:15;
then a' 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,b' <> Line b,a'

proof

assume Line a,b' = Line b,a' ; :: thesis: contradiction
then LIN a',b',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,b' // b,c by A40, A33, A34, A42, AFF_1:53;
then b,a' // b,c by A12, A31, AFF_1:14;
then LIN b,a',c by AFF_1:def 1;
then LIN b,c,a' by AFF_1:15;
then a' 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,b' // Line b,a' by A12, A31, A38, AFF_1:51;
a,s // b',c by A15, A19, A20, A43, AFF_1:53;
then A51: b,s // a',c by A1, A32, A40, A44, A39, A33, A34, A35, A42, A36, A48, A41, A50, Def11;
b',a // c,s by A40, A33, A34, A42, AFF_1:53;
then c',a // b,s by A1, A18, A17, A26, A15, A19, A20, A21, A43, A37, A30, A25, A27, Def11;
then c',a // a',c by A51, A49, AFF_1:14;
hence contradiction by A22, AFF_1:13; :: thesis: verum

end;