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
A23: now :: thesis: not a = c
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;
A25: Line (c,b9) <> C9
proof
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;
A26: c9 in Line (b,c9) by A16, AFF_1:24;
then A27: Line (c,b9) // Line (b,c9) by A13, A16, A14, A18, A17, A15, AFF_1:38;
A28: now :: thesis: not b = c
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;
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: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;
A31: a <> b9 by A4, A7, A8, A10, AFF_1:45;
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
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;
not C // C9
proof
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 consider s being Element of AP such that
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;
A47: now :: thesis: not a9 = b9
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;
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: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;
A49: b <> s
proof
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;
A50: Line (a,b9) // Line (b,a9) by A12, A31, A38, AFF_1:37;
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