let AP be AffinPlane; :: thesis: ( AP is translational iff AP is satisfying_des_1 )

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

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

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)

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

A80: x <> c9

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

hereby :: thesis: ( AP is satisfying_des_1 implies AP is translational )

assume A32:
AP is satisfying_des_1
; :: thesis: AP is translational assume A1:
AP is translational
; :: thesis: AP is satisfying_des_1

thus AP is satisfying_des_1 :: thesis: verum

end;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

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

proof

A24:
A <> K
assume
a,c // K
; :: thesis: contradiction

then a,c // A by A20, AFF_1:43;

then A23: c in A by A3, A8, AFF_1:23;

a9,c9 // a,c by A14, AFF_1:4;

then a9,c9 // A by A3, A8, A21, A23, AFF_1:27;

then c9 in A by A4, A8, AFF_1:23;

hence contradiction by A7, A8, A10, A12, A17, A23, AFF_1:18; :: thesis: verum

end;then a,c // A by A20, AFF_1:43;

then A23: c in A by A3, A8, AFF_1:23;

a9,c9 // a,c by A14, AFF_1:4;

then a9,c9 // A by A3, A8, A21, A23, AFF_1:27;

then c9 in A by A4, A8, AFF_1:23;

hence contradiction by A7, A8, A10, A12, A17, A23, AFF_1:18; :: thesis: verum

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

A26: now :: thesis: not b9 = c9

A27:
K is being_line
by A20, AFF_1:36;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;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

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

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

A59:
c in Line (a,c)
by A50, AFF_1:24;
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;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

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

A66:
not Line (a,c) // M
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;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

proof

A67:
Line (a,c) is being_line
by A50, AFF_1:24;
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;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

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

A73:
x in Line (x,c9)
by AFF_1:15;
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;then c9 in A by AFF_1:15;

hence contradiction by A34, A40, A45, AFF_1:45; :: thesis: verum

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

A79:
P // C
by A33, A34, AFF_1:44;
A77:
a <> x

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;proof

assume
LIN a,b,x
; :: thesis: contradiction
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;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

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

A80: x <> c9

proof

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;A81: now :: thesis: not P = Line (b9,c9)

assume
x = c9
; :: thesis: contradictionA82:
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 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

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

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