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, a', b', c' 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 & 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 AP; :: thesis: for a, b, c, a', b', c' 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 & 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 AP; :: 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 A2: ( 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' ) ; :: thesis: a,c' // c,a'
assume A3: not a,c' // c,a' ; :: thesis: contradiction
A4: ( b <> c' & c <> b' & a <> b' & b <> a' ) by A2, AFF_1:59;
A5: ( a <> b & a <> c & b <> c )
proof
A6: now
assume A7: a = b ; :: thesis: contradiction
then LIN a,b',a' by A2, AFF_1:def 1;
then LIN a',b',a by AFF_1:15;
then ( a' = b' or a in N ) by A2, AFF_1:39;
hence contradiction by A2, A3, A7, AFF_1:59; :: thesis: verum
end;
A8: now
assume A9: a = c ; :: thesis: contradiction
then b,c' // b,a' by A2, A4, 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 A2, AFF_1:39;
hence contradiction by A2, A3, A9, AFF_1:11, AFF_1:59; :: thesis: verum
end;
now
assume A10: b = c ; :: thesis: contradiction
then LIN b,c',b' by A2, AFF_1:def 1;
then LIN b',c',b by AFF_1:15;
then ( b' = c' or b in N ) by A2, AFF_1:39;
hence contradiction by A2, A3, A10, AFF_1:59; :: thesis: verum
end;
hence ( a <> b & a <> c & b <> c ) by A6, A8; :: thesis: verum
end;
A11: ( a' <> b' & a' <> c' & b' <> c' )
proof
A12: now
assume a' = b' ; :: thesis: contradiction
then a',a // a',b by A2, 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, A5, AFF_1:39;
hence contradiction by A2, AFF_1:59; :: thesis: verum
end;
A13: now
assume a' = c' ; :: thesis: contradiction
then a,b' // c,b' by A2, A4, AFF_1:14;
then b',a // b',c by AFF_1:13;
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, A5, AFF_1:39;
hence contradiction by A2, AFF_1:59; :: thesis: verum
end;
hence ( a' <> b' & a' <> c' & b' <> c' ) by A12, A13; :: thesis: verum
end;
set A = Line a,b';
set A' = Line b,a';
set P = Line b,c';
set P' = Line c,b';
A14: ( Line a,b' is being_line & Line b,a' is being_line & Line b,c' is being_line & Line c,b' is being_line & a in Line a,b' & b' in Line a,b' & b in Line b,a' & a' in Line b,a' & b in Line b,c' & c' in Line b,c' & c in Line c,b' & b' in Line c,b' ) by A4, AFF_1:38;
then consider C being Subset of AP such that
A15: ( c in C & Line a,b' // C ) by AFF_1:63;
A16: ( C is being_line & C // Line a,b' ) by A15, AFF_1:50;
consider C' being Subset of AP such that
A17: ( a in C' & Line c,b' // C' ) by A14, AFF_1:63;
A18: ( C' is being_line & C' // Line c,b' ) by A17, AFF_1:50;
not C // C'
proof
assume C // C' ; :: thesis: contradiction
then Line a,b' // C' by A15, AFF_1:58;
then Line a,b' // Line c,b' by A17, AFF_1:58;
then b',a // b',c by A14, 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, A5, AFF_1:39;
hence contradiction by A2, AFF_1:59; :: thesis: verum
end;
then consider s being Element of AP such that
A19: ( s in C & s in C' ) by A16, A18, AFF_1:72;
A20: b',a // c,s by A14, A15, A19, AFF_1:53;
A21: b',c' // c,b by A2, AFF_1:53;
A22: Line c,b' <> Line b,c'
proof
assume Line c,b' = Line b,c' ; :: thesis: contradiction
then LIN b,c,b' by A14, AFF_1:33;
then b' in M by A2, A5, AFF_1:39;
hence contradiction by A2, AFF_1:59; :: thesis: verum
end;
A23: Line c,b' <> C'
proof
assume Line c,b' = C' ; :: thesis: contradiction
then LIN a,c,b' by A14, A17, AFF_1:33;
then b' in M by A2, A5, AFF_1:39;
hence contradiction by A2, AFF_1:59; :: thesis: verum
end;
Line c,b' // Line b,c' by A2, A4, A14, AFF_1:52;
then A24: c',a // b,s by A1, A14, A17, A18, A19, A20, A21, A22, A23, Def11;
A25: a,b // b',a' by A2, AFF_1:53;
A26: Line a,b' <> Line b,a'
proof
assume Line a,b' = Line b,a' ; :: thesis: contradiction
then LIN a',b',a by A14, AFF_1:33;
then a in N by A2, A11, AFF_1:39;
hence contradiction by A2, AFF_1:59; :: thesis: verum
end;
A27: Line a,b' <> C
proof
assume Line a,b' = C ; :: thesis: contradiction
then LIN a,c,b' by A14, A15, AFF_1:33;
then b' in M by A2, A5, AFF_1:39;
hence contradiction by A2, AFF_1:59; :: thesis: verum
end;
A28: Line a,b' // Line b,a' by A2, A4, AFF_1:51;
a,s // b',c by A14, A17, A19, AFF_1:53;
then A29: b,s // a',c by A1, A14, A15, A16, A19, A25, A26, A27, A28, Def11;
b <> s
proof
assume b = s ; :: thesis: contradiction
then a,b' // b,c by A14, A15, A19, AFF_1:53;
then b,a' // b,c by A2, A4, 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, AFF_1:39;
hence contradiction by A2, AFF_1:59; :: thesis: verum
end;
then c',a // a',c by A24, A29, AFF_1:14;
hence contradiction by A3, AFF_1:13; :: thesis: verum
end;