let AP be AffinPlane; :: thesis: ( AP is translational implies AP is satisfying_pap )

assume A1: AP is translational ; :: thesis: AP is satisfying_pap

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:45;

then A15: ( c in Line (c,b9) & b9 in Line (c,b9) ) by AFF_1:24;

A16: b <> c9 by A5, A7, A8, A11, AFF_1:45;

then A17: ( Line (b,c9) is being_line & b in Line (b,c9) ) by AFF_1:24;

A18: Line (c,b9) is being_line by A14, AFF_1:24;

then consider C9 being Subset of AP such that

A19: a in C9 and

A20: Line (c,b9) // C9 by AFF_1:49;

A21: C9 is being_line by A20, AFF_1:36;

assume A22: not a,c9 // c,a9 ; :: thesis: contradiction

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

then A32: Line (a,b9) is being_line by AFF_1:24;

then consider C being Subset of AP such that

A33: c in C and

A34: Line (a,b9) // C by AFF_1:49;

A35: C is being_line by A34, AFF_1:36;

A36: a,b // b9,a9 by A4, A5, A7, A9, A10, AFF_1:39;

A37: b9,c9 // c,b by A5, A6, A7, A10, A11, AFF_1:39;

A38: b <> a9 by A5, A7, A8, A9, AFF_1:45;

then A39: a9 in Line (b,a9) by AFF_1:24;

A40: ( a in Line (a,b9) & b9 in Line (a,b9) ) by A31, AFF_1:24;

A41: Line (a,b9) <> C

A42: s in C and

A43: s in C9 by A35, A21, AFF_1:58;

A44: ( Line (b,a9) is being_line & b in Line (b,a9) ) by A38, AFF_1:24;

a,s // b9,c by A15, A19, A20, A43, AFF_1:39;

then A51: b,s // a9,c by A1, A32, A40, A44, A39, A33, A34, A35, A42, A36, A48, A41, A50;

b9,a // c,s by A40, A33, A34, A42, AFF_1:39;

then c9,a // b,s by A1, A18, A17, A26, A15, A19, A20, A21, A43, A37, A30, A25, A27;

then c9,a // a9,c by A51, A49, AFF_1:5;

hence contradiction by A22, AFF_1:4; :: thesis: verum

assume A1: AP is translational ; :: thesis: AP is satisfying_pap

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:45;

then A15: ( c in Line (c,b9) & b9 in Line (c,b9) ) by AFF_1:24;

A16: b <> c9 by A5, A7, A8, A11, AFF_1:45;

then A17: ( Line (b,c9) is being_line & b in Line (b,c9) ) by AFF_1:24;

A18: Line (c,b9) is being_line by A14, AFF_1:24;

then consider C9 being Subset of AP such that

A19: a in C9 and

A20: Line (c,b9) // C9 by AFF_1:49;

A21: C9 is being_line by A20, AFF_1:36;

assume A22: not a,c9 // c,a9 ; :: thesis: contradiction

A23: now :: thesis: not a = c

A25:
Line (c,b9) <> C9
assume A24:
a = c
; :: thesis: contradiction

then b,c9 // b,a9 by A12, A13, A14, AFF_1:5;

then LIN b,c9,a9 by AFF_1:def 1;

then LIN a9,c9,b by AFF_1:6;

then ( a9 = c9 or b in N ) by A3, A9, A11, AFF_1:25;

hence contradiction by A5, A7, A8, A22, A24, AFF_1:2, AFF_1:45; :: thesis: verum

end;then b,c9 // b,a9 by A12, A13, A14, AFF_1:5;

then LIN b,c9,a9 by AFF_1:def 1;

then LIN a9,c9,b by AFF_1:6;

then ( a9 = c9 or b in N ) by A3, A9, A11, AFF_1:25;

hence contradiction by A5, A7, A8, A22, A24, AFF_1:2, AFF_1:45; :: thesis: verum

proof

A26:
c9 in Line (b,c9)
by A16, AFF_1:24;
assume
Line (c,b9) = C9
; :: thesis: contradiction

then LIN a,c,b9 by A18, A15, A19, AFF_1:21;

then b9 in M by A2, A4, A6, A23, AFF_1:25;

hence contradiction by A7, A8, A10, AFF_1:45; :: thesis: verum

end;then LIN a,c,b9 by A18, A15, A19, AFF_1:21;

then b9 in M by A2, A4, A6, A23, AFF_1:25;

hence contradiction by A7, A8, A10, AFF_1:45; :: thesis: verum

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

A28: now :: thesis: not b = c

A30:
Line (c,b9) <> Line (b,c9)
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:6;

then ( b9 = c9 or b in N ) by A3, A10, A11, AFF_1:25;

hence contradiction by A5, A7, A8, A12, A22, A29, AFF_1:45; :: thesis: verum

end;then LIN b,c9,b9 by A13, AFF_1:def 1;

then LIN b9,c9,b by AFF_1:6;

then ( b9 = c9 or b in N ) by A3, A10, A11, AFF_1:25;

hence contradiction by A5, A7, A8, A12, A22, A29, AFF_1:45; :: thesis: verum

proof

A31:
a <> b9
by A4, A7, A8, A10, AFF_1:45;
assume
Line (c,b9) = Line (b,c9)
; :: thesis: contradiction

then LIN b,c,b9 by A17, A15, AFF_1:21;

then b9 in M by A2, A5, A6, A28, AFF_1:25;

hence contradiction by A7, A8, A10, AFF_1:45; :: thesis: verum

end;then LIN b,c,b9 by A17, A15, AFF_1:21;

then b9 in M by A2, A5, A6, A28, AFF_1:25;

hence contradiction by A7, A8, A10, AFF_1:45; :: thesis: verum

then A32: Line (a,b9) is being_line by AFF_1:24;

then consider C being Subset of AP such that

A33: c in C and

A34: Line (a,b9) // C by AFF_1:49;

A35: C is being_line by A34, AFF_1:36;

A36: a,b // b9,a9 by A4, A5, A7, A9, A10, AFF_1:39;

A37: b9,c9 // c,b by A5, A6, A7, A10, A11, AFF_1:39;

A38: b <> a9 by A5, A7, A8, A9, AFF_1:45;

then A39: a9 in Line (b,a9) by AFF_1:24;

A40: ( a in Line (a,b9) & b9 in Line (a,b9) ) by A31, AFF_1:24;

A41: Line (a,b9) <> C

proof

not C // C9
assume
Line (a,b9) = C
; :: thesis: contradiction

then LIN a,c,b9 by A32, A40, A33, AFF_1:21;

then b9 in M by A2, A4, A6, A23, AFF_1:25;

hence contradiction by A7, A8, A10, AFF_1:45; :: thesis: verum

end;then LIN a,c,b9 by A32, A40, A33, AFF_1:21;

then b9 in M by A2, A4, A6, A23, AFF_1:25;

hence contradiction by A7, A8, A10, AFF_1:45; :: thesis: verum

proof

then consider s being Element of AP such that
assume
C // C9
; :: thesis: contradiction

then Line (a,b9) // C9 by A34, AFF_1:44;

then Line (a,b9) // Line (c,b9) by A20, AFF_1:44;

then b9,a // b9,c by A40, A15, AFF_1:39;

then LIN b9,a,c by AFF_1:def 1;

then LIN a,c,b9 by AFF_1:6;

then b9 in M by A2, A4, A6, A23, AFF_1:25;

hence contradiction by A7, A8, A10, AFF_1:45; :: thesis: verum

end;then Line (a,b9) // C9 by A34, AFF_1:44;

then Line (a,b9) // Line (c,b9) by A20, AFF_1:44;

then b9,a // b9,c by A40, A15, AFF_1:39;

then LIN b9,a,c by AFF_1:def 1;

then LIN a,c,b9 by AFF_1:6;

then b9 in M by A2, A4, A6, A23, AFF_1:25;

hence contradiction by A7, A8, A10, AFF_1:45; :: thesis: verum

A42: s in C and

A43: s in C9 by A35, A21, AFF_1:58;

A44: ( Line (b,a9) is being_line & b in Line (b,a9) ) by A38, AFF_1:24;

A45: now :: thesis: not a = b

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:6;

then ( a9 = b9 or a in N ) by A3, A9, A10, AFF_1:25;

hence contradiction by A4, A7, A8, A13, A22, A46, AFF_1:45; :: thesis: verum

end;then LIN a,b9,a9 by A12, AFF_1:def 1;

then LIN a9,b9,a by AFF_1:6;

then ( a9 = b9 or a in N ) by A3, A9, A10, AFF_1:25;

hence contradiction by A4, A7, A8, A13, A22, A46, AFF_1:45; :: thesis: verum

A47: now :: thesis: not a9 = b9

A48:
Line (a,b9) <> Line (b,a9)
assume
a9 = b9
; :: thesis: contradiction

then a9,a // a9,b by A12, AFF_1:4;

then LIN a9,a,b by AFF_1:def 1;

then LIN a,b,a9 by AFF_1:6;

then a9 in M by A2, A4, A5, A45, AFF_1:25;

hence contradiction by A7, A8, A9, AFF_1:45; :: thesis: verum

end;then a9,a // a9,b by A12, AFF_1:4;

then LIN a9,a,b by AFF_1:def 1;

then LIN a,b,a9 by AFF_1:6;

then a9 in M by A2, A4, A5, A45, AFF_1:25;

hence contradiction by A7, A8, A9, AFF_1:45; :: thesis: verum

proof

A49:
b <> s
assume
Line (a,b9) = Line (b,a9)
; :: thesis: contradiction

then LIN a9,b9,a by A32, A40, A39, AFF_1:21;

then a in N by A3, A9, A10, A47, AFF_1:25;

hence contradiction by A4, A7, A8, AFF_1:45; :: thesis: verum

end;then LIN a9,b9,a by A32, A40, A39, AFF_1:21;

then a in N by A3, A9, A10, A47, AFF_1:25;

hence contradiction by A4, A7, A8, AFF_1:45; :: thesis: verum

proof

A50:
Line (a,b9) // Line (b,a9)
by A12, A31, A38, AFF_1:37;
assume
b = s
; :: thesis: contradiction

then a,b9 // b,c by A40, A33, A34, A42, AFF_1:39;

then b,a9 // b,c by A12, A31, AFF_1:5;

then LIN b,a9,c by AFF_1:def 1;

then LIN b,c,a9 by AFF_1:6;

then a9 in M by A2, A5, A6, A28, AFF_1:25;

hence contradiction by A7, A8, A9, AFF_1:45; :: thesis: verum

end;then a,b9 // b,c by A40, A33, A34, A42, AFF_1:39;

then b,a9 // b,c by A12, A31, AFF_1:5;

then LIN b,a9,c by AFF_1:def 1;

then LIN b,c,a9 by AFF_1:6;

then a9 in M by A2, A5, A6, A28, AFF_1:25;

hence contradiction by A7, A8, A9, AFF_1:45; :: thesis: verum

a,s // b9,c by A15, A19, A20, A43, AFF_1:39;

then A51: b,s // a9,c by A1, A32, A40, A44, A39, A33, A34, A35, A42, A36, A48, A41, A50;

b9,a // c,s by A40, A33, A34, A42, AFF_1:39;

then c9,a // b,s by A1, A18, A17, A26, A15, A19, A20, A21, A43, A37, A30, A25, A27;

then c9,a // a9,c by A51, A49, AFF_1:5;

hence contradiction by A22, AFF_1:4; :: thesis: verum