let AP be AffinPlane; :: thesis: ( AP is translational iff AP is satisfying_des_1 )
hereby :: thesis: ( AP is satisfying_des_1 implies AP is translational )
assume A1: AP is translational ; :: thesis: AP is satisfying_des_1
thus AP is satisfying_des_1 :: thesis: verum
proof
let A be Subset of AP; :: according to AFF_2:def 12 :: thesis: for P, C being Subset of AP
for a, b, c, a9, b9, c9 being Element of AP st A // P & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 & b,c // b9,c9 & not LIN a,b,c & c <> c9 holds
A // C
let P, C be Subset of AP; :: thesis: for a, b, c, a9, b9, c9 being Element of AP st A // P & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 & b,c // b9,c9 & not LIN a,b,c & c <> c9 holds
A // C
let a, b, c, a9, b9, c9 be Element of AP; :: thesis: ( A // P & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 & b,c // b9,c9 & not LIN a,b,c & c <> c9 implies A // C )
assume that
A2: A // P and
A3: a in A and
A4: a9 in A and
A5: b in P and
A6: b9 in P and
A7: ( c in C & c9 in C ) and
A8: A is being_line and
A9: P is being_line and
A10: C is being_line and
A11: A <> P and
A12: A <> C and
A13: a,b // a9,b9 and
A14: a,c // a9,c9 and
A15: b,c // b9,c9 and
A16: not LIN a,b,c and
A17: c <> c9 ; :: thesis: A // C
assume A18: not A // C ; :: thesis: contradiction
consider K being Subset of AP such that
A19: c9 in K and
A20: A // K by A8, AFF_1:49;
A21: a <> c by A16, AFF_1:7;
A22: not a,c // K A24: A <> K
proof
assume A25: A = K ; :: thesis: contradiction
a9,c9 // a,c by A14, AFF_1:4;
then a9 = c9 by A4, A19, A20, A22, A25, AFF_1:32, AFF_1:40;
then a9,b9 // b,c by A15, AFF_1:4;
then ( a9 = b9 or a,b // b,c ) by A13, AFF_1:5;
then ( b9 in A or b,a // b,c ) by A4, AFF_1:4;
then LIN b,a,c by A2, A6, A11, AFF_1:45, AFF_1:def 1;
hence contradiction by A16, AFF_1:6; :: thesis: verum
end;
A26: now :: thesis: not b9 = c9
assume b9 = c9 ; :: thesis: contradiction
then ( a,b // a,c or a9 = b9 ) by A13, A14, AFF_1:5;
hence contradiction by A2, A4, A6, A11, A16, AFF_1:45, AFF_1:def 1; :: thesis: verum
end;
A27: K is being_line by A20, AFF_1:36;
then consider x being Element of AP such that
A28: x in K and
A29: LIN a,c,x by A22, AFF_1:59;
a,c // a,x by A29, AFF_1:def 1;
then a,x // a9,c9 by A14, A21, AFF_1:5;
then b,x // b9,c9 by A1, A2, A3, A4, A5, A6, A8, A9, A11, A13, A19, A20, A27, A28, A24;
then ( b,x // b,c or b9 = c9 ) by A15, AFF_1:5;
then LIN b,x,c by A26, AFF_1:def 1;
then A30: LIN x,c,b by AFF_1:6;
A31: LIN x,c,c by AFF_1:7;
LIN x,c,a by A29, AFF_1:6;
then c in K by A16, A28, A30, A31, AFF_1:8;
hence contradiction by A7, A10, A17, A18, A19, A20, A27, AFF_1:18; :: thesis: verum
end;
end;
assume A32: AP is satisfying_des_1 ; :: thesis: AP is translational
let A be Subset of AP; :: according to AFF_2:def 11 :: thesis: for P, C being Subset of AP
for a, b, c, a9, b9, c9 being Element of AP st A // P & A // C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 holds
b,c // b9,c9
let P, C be Subset of AP; :: thesis: for a, b, c, a9, b9, c9 being Element of AP st A // P & A // C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 holds
b,c // b9,c9
let a, b, c, a9, b9, c9 be Element of AP; :: thesis: ( A // P & A // C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 implies b,c // b9,c9 )
assume that
A33: A // P and
A34: A // C and
A35: a in A and
A36: a9 in A and
A37: b in P and
A38: b9 in P and
A39: c in C and
A40: c9 in C and
A41: A is being_line and
A42: P is being_line and
A43: C is being_line and
A44: A <> P and
A45: A <> C and
A46: a,b // a9,b9 and
A47: a,c // a9,c9 ; :: thesis: b,c // b9,c9
A48: a <> b by A33, A35, A37, A44, AFF_1:45;
A49: a9 <> b9 by A33, A36, A38, A44, AFF_1:45;
set K = Line (a,c);
set N = Line (b9,c9);
A50: a <> c by A34, A35, A39, A45, AFF_1:45;
then A51: a in Line (a,c) by AFF_1:24;
assume A52: not b,c // b9,c9 ; :: thesis: contradiction
then A53: b9 <> c9 by AFF_1:3;
then A54: b9 in Line (b9,c9) by AFF_1:24;
A55: b <> c by A52, AFF_1:3;
A56: not LIN a,b,c
proof
assume A57: LIN a,b,c ; :: thesis: contradiction
then LIN b,c,a by AFF_1:6;
then b,c // b,a by AFF_1:def 1;
then b,c // a,b by AFF_1:4;
then A58: b,c // a9,b9 by A46, A48, AFF_1:5;
LIN c,b,a by A57, AFF_1:6;
then c,b // c,a by AFF_1:def 1;
then b,c // a,c by AFF_1:4;
then b,c // a9,c9 by A47, A50, AFF_1:5;
then a9,c9 // a9,b9 by A55, A58, AFF_1:5;
then LIN a9,c9,b9 by AFF_1:def 1;
then LIN b9,c9,a9 by AFF_1:6;
then b9,c9 // b9,a9 by AFF_1:def 1;
then b9,c9 // a9,b9 by AFF_1:4;
hence contradiction by A52, A49, A58, AFF_1:5; :: thesis: verum
end;
A59: c in Line (a,c) by A50, AFF_1:24;
A60: Line (b9,c9) is being_line by A53, AFF_1:24;
then consider M being Subset of AP such that
A61: b in M and
A62: Line (b9,c9) // M by AFF_1:49;
A63: c9 in Line (b9,c9) by A53, AFF_1:24;
A64: a9 <> c9 by A34, A36, A40, A45, AFF_1:45;
A65: not LIN a9,b9,c9
proof
assume LIN a9,b9,c9 ; :: thesis: contradiction
then a9,b9 // a9,c9 by AFF_1:def 1;
then a,b // a9,c9 by A46, A49, AFF_1:5;
then a,b // a,c by A47, A64, AFF_1:5;
hence contradiction by A56, AFF_1:def 1; :: thesis: verum
end;
A66: not Line (a,c) // M
proof
assume Line (a,c) // M ; :: thesis: contradiction
then Line (a,c) // Line (b9,c9) by A62, AFF_1:44;
then a,c // b9,c9 by A51, A59, A54, A63, AFF_1:39;
then a9,c9 // b9,c9 by A47, A50, AFF_1:5;
then c9,a9 // c9,b9 by AFF_1:4;
then LIN c9,a9,b9 by AFF_1:def 1;
hence contradiction by A65, AFF_1:6; :: thesis: verum
end;
A67: Line (a,c) is being_line by A50, AFF_1:24;
A68: M is being_line by A62, AFF_1:36;
then consider x being Element of AP such that
A69: x in Line (a,c) and
A70: x in M by A67, A66, AFF_1:58;
A71: b,x // b9,c9 by A54, A63, A61, A62, A70, AFF_1:39;
set D = Line (x,c9);
A72: A <> Line (x,c9)
proof
assume A = Line (x,c9) ; :: thesis: contradiction
then c9 in A by AFF_1:15;
hence contradiction by A34, A40, A45, AFF_1:45; :: thesis: verum
end;
A73: x in Line (x,c9) by AFF_1:15;
LIN a,c,x by A67, A51, A59, A69, AFF_1:21;
then a,c // a,x by AFF_1:def 1;
then A74: a,x // a9,c9 by A47, A50, AFF_1:5;
A75: c9 in Line (x,c9) by AFF_1:15;
A76: not LIN a,b,x
proof
A77: a <> x
proof
assume a = x ; :: thesis: contradiction
then a,b // b9,c9 by A54, A63, A61, A62, A70, AFF_1:39;
then a9,b9 // b9,c9 by A46, A48, AFF_1:5;
then b9,a9 // b9,c9 by AFF_1:4;
then LIN b9,a9,c9 by AFF_1:def 1;
hence contradiction by A65, AFF_1:6; :: thesis: verum
end;
assume LIN a,b,x ; :: thesis: contradiction
then LIN x,b,a by AFF_1:6;
then A78: x,b // x,a by AFF_1:def 1;
x <> b by A67, A51, A59, A56, A69, AFF_1:21;
hence contradiction by A67, A51, A61, A68, A66, A69, A70, A78, A77, AFF_1:38; :: thesis: verum
end;
A79: P // C by A33, A34, AFF_1:44;
A80: x <> c9
proof
A81: now :: thesis: not P = Line (b9,c9)
A82: P // P by A33, AFF_1:44;
assume A83: P = Line (b9,c9) ; :: thesis: contradiction
then c in P by A39, A40, A79, A63, AFF_1:45;
hence contradiction by A37, A38, A52, A63, A83, A82, AFF_1:39; :: thesis: verum
end;
assume x = c9 ; :: thesis: contradiction
then M = Line (b9,c9) by A63, A62, A70, AFF_1:45;
then A84: ( P = Line (b9,c9) or b = b9 ) by A37, A38, A42, A60, A54, A61, AFF_1:18;
then b,a // b,a9 by A46, A81, AFF_1:4;
then LIN b,a,a9 by AFF_1:def 1;
then LIN a,a9,b by AFF_1:6;
then ( b in A or a = a9 ) by A35, A36, A41, AFF_1:25;
then LIN a9,c,c9 by A33, A37, A44, A47, AFF_1:45, AFF_1:def 1;
then LIN c,c9,a9 by AFF_1:6;
then ( c = c9 or a9 in C ) by A39, A40, A43, AFF_1:25;
hence contradiction by A34, A36, A45, A52, A84, A81, AFF_1:2, AFF_1:45; :: thesis: verum
end;
then Line (x,c9) is being_line by AFF_1:24;
then A // Line (x,c9) by A32, A33, A35, A36, A37, A38, A41, A42, A44, A46, A71, A74, A73, A75, A80, A76, A72;
then Line (x,c9) // C by A34, AFF_1:44;
then C = Line (x,c9) by A40, A75, AFF_1:45;
then C = Line (a,c) by A39, A43, A52, A67, A59, A69, A71, A73, AFF_1:18;
hence contradiction by A34, A35, A45, A51, AFF_1:45; :: thesis: verum