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

A1: now

assume A2: AP is satisfying_des_1 ; :: thesis: AP is translational
thus AP is translational :: thesis: verum

proof

let A be Subset of ; :: according to AFF_2:def 11 :: thesis: for P, C being Subset of
for a, b, c, a', b', c' being Element of st A // P & A // C & a in A & a' in A & b in P & b' in P & c in C & c' in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a',b' & a,c // a',c' holds
b,c // b',c'
let P, C be Subset of ; :: thesis: for a, b, c, a', b', c' being Element of st A // P & A // C & a in A & a' in A & b in P & b' in P & c in C & c' in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a',b' & a,c // a',c' holds
b,c // b',c'
let a, b, c, a', b', c' be Element of ; :: thesis: ( A // P & A // C & a in A & a' in A & b in P & b' in P & c in C & c' in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a',b' & a,c // a',c' implies b,c // b',c' )
assume that
A3: A // P and
A4: A // C and
A5: a in A and
A6: a' in A and
A7: b in P and
A8: b' in P and
A9: c in C and
A10: c' in C and
A11: A is being_line and
A12: P is being_line and
A13: C is being_line and
A14: A <> P and
A15: A <> C and
A16: a,b // a',b' and
A17: a,c // a',c' ; :: thesis: b,c // b',c'
A18: a <> b by A3, A5, A7, A14, AFF_1:59;
A19: a' <> b' by A3, A6, A8, A14, AFF_1:59;
set K = Line a,c;
set N = Line b',c';
A20: a <> c by A4, A5, A9, A15, AFF_1:59;
then A21: a in Line a,c by AFF_1:38;
assume A22: not b,c // b',c' ; :: thesis: contradiction
then A23: b' <> c' by AFF_1:12;
then A24: b' in Line b',c' by AFF_1:38;
A25: b <> c by A22, AFF_1:12;
A26: not LIN a,b,c

proof

assume A27: LIN a,b,c ; :: thesis: contradiction
then LIN b,c,a by AFF_1:15;
then b,c // b,a by AFF_1:def 1;
then b,c // a,b by AFF_1:13;
then A28: b,c // a',b' by A16, A18, AFF_1:14;
LIN c,b,a by A27, AFF_1:15;
then c,b // c,a by AFF_1:def 1;
then b,c // a,c by AFF_1:13;
then b,c // a',c' by A17, A20, AFF_1:14;
then a',c' // a',b' by A25, A28, AFF_1:14;
then LIN a',c',b' by AFF_1:def 1;
then LIN b',c',a' by AFF_1:15;
then b',c' // b',a' by AFF_1:def 1;
then b',c' // a',b' by AFF_1:13;
hence contradiction by A22, A19, A28, AFF_1:14; :: thesis: verum

end;

A29: c in Line a,c by A20, AFF_1:38;
A30: Line b',c' is being_line by A23, AFF_1:38;
then consider M being Subset of such that
A31: b in M and
A32: Line b',c' // M by AFF_1:63;
A33: c' in Line b',c' by A23, AFF_1:38;
A34: a' <> c' by A4, A6, A10, A15, AFF_1:59;
A35: not LIN a',b',c'

proof

assume LIN a',b',c' ; :: thesis: contradiction
then a',b' // a',c' by AFF_1:def 1;
then a,b // a',c' by A16, A19, AFF_1:14;
then a,b // a,c by A17, A34, AFF_1:14;
hence contradiction by A26, AFF_1:def 1; :: thesis: verum

end;

A36: not Line a,c // M

proof

assume Line a,c // M ; :: thesis: contradiction
then Line a,c // Line b',c' by A32, AFF_1:58;
then a,c // b',c' by A21, A29, A24, A33, AFF_1:53;
then a',c' // b',c' by A17, A20, AFF_1:14;
then c',a' // c',b' by AFF_1:13;
then LIN c',a',b' by AFF_1:def 1;
hence contradiction by A35, AFF_1:15; :: thesis: verum

end;

A37: Line a,c is being_line by A20, AFF_1:38;
A38: M is being_line by A32, AFF_1:50;
then consider x being Element of such that
A39: x in Line a,c and
A40: x in M by A37, A36, AFF_1:72;
A41: b,x // b',c' by A24, A33, A31, A32, A40, AFF_1:53;
set D = Line x,c';
A42: A <> Line x,c'

proof

assume A = Line x,c' ; :: thesis: contradiction
then c' in A by AFF_1:26;
hence contradiction by A4, A10, A15, AFF_1:59; :: thesis: verum

end;

A43: x in Line x,c' by AFF_1:26;
LIN a,c,x by A37, A21, A29, A39, AFF_1:33;
then a,c // a,x by AFF_1:def 1;
then A44: a,x // a',c' by A17, A20, AFF_1:14;
A45: c' in Line x,c' by AFF_1:26;
A46: not LIN a,b,x

proof

A47: a <> x

proof

assume a = x ; :: thesis: contradiction
then a,b // b',c' by A24, A33, A31, A32, A40, AFF_1:53;
then a',b' // b',c' by A16, A18, AFF_1:14;
then b',a' // b',c' by AFF_1:13;
then LIN b',a',c' by AFF_1:def 1;
hence contradiction by A35, AFF_1:15; :: thesis: verum

end;

assume LIN a,b,x ; :: thesis: contradiction
then LIN x,b,a by AFF_1:15;
then A48: x,b // x,a by AFF_1:def 1;
x <> b by A37, A21, A29, A26, A39, AFF_1:33;
hence contradiction by A37, A21, A31, A38, A36, A39, A40, A48, A47, AFF_1:52; :: thesis: verum

end;

A49: P // C by A3, A4, AFF_1:58;
A50: x <> c'

proof

A51: now

A52: P // P by A3, AFF_1:58;
assume A53: P = Line b',c' ; :: thesis: contradiction
then c in P by A9, A10, A49, A33, AFF_1:59;
hence contradiction by A7, A8, A22, A33, A53, A52, AFF_1:53; :: thesis: verum

end;

assume x = c' ; :: thesis: contradiction
then M = Line b',c' by A33, A32, A40, AFF_1:59;
then A54: ( P = Line b',c' or b = b' ) by A7, A8, A12, A30, A24, A31, AFF_1:30;
then b,a // b,a' by A16, A51, AFF_1:13;
then LIN b,a,a' by AFF_1:def 1;
then LIN a,a',b by AFF_1:15;
then ( b in A or a = a' ) by A5, A6, A11, AFF_1:39;
then LIN a',c,c' by A3, A7, A14, A17, AFF_1:59, AFF_1:def 1;
then LIN c,c',a' by AFF_1:15;
then ( c = c' or a' in C ) by A9, A10, A13, AFF_1:39;
hence contradiction by A4, A6, A15, A22, A54, A51, AFF_1:11, AFF_1:59; :: thesis: verum

end;

then Line x,c' is being_line by AFF_1:38;
then A // Line x,c' by A2, A3, A5, A6, A7, A8, A11, A12, A14, A16, A41, A44, A43, A45, A50, A46, A42, Def12;
then Line x,c' // C by A4, AFF_1:58;
then C = Line x,c' by A10, A45, AFF_1:59;
then C = Line a,c by A9, A13, A22, A37, A29, A39, A41, A43, AFF_1:30;
hence contradiction by A4, A5, A15, A21, AFF_1:59; :: thesis: verum

end;

end;

now

assume A55: AP is translational ; :: thesis: AP is satisfying_des_1
thus AP is satisfying_des_1 :: thesis: verum

proof

let A be Subset of ; :: according to AFF_2:def 12 :: thesis: for P, C being Subset of
for a, b, c, a', b', c' being Element of st A // P & a in A & a' in A & b in P & b' in P & c in C & c' in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a',b' & a,c // a',c' & b,c // b',c' & not LIN a,b,c & c <> c' holds
A // C
let P, C be Subset of ; :: thesis: for a, b, c, a', b', c' being Element of st A // P & a in A & a' in A & b in P & b' in P & c in C & c' in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a',b' & a,c // a',c' & b,c // b',c' & not LIN a,b,c & c <> c' holds
A // C
let a, b, c, a', b', c' be Element of ; :: thesis: ( A // P & a in A & a' in A & b in P & b' in P & c in C & c' in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a',b' & a,c // a',c' & b,c // b',c' & not LIN a,b,c & c <> c' implies A // C )
assume that
A56: A // P and
A57: a in A and
A58: a' in A and
A59: b in P and
A60: b' in P and
A61: ( c in C & c' in C ) and
A62: A is being_line and
A63: P is being_line and
A64: C is being_line and
A65: A <> P and
A66: A <> C and
A67: a,b // a',b' and
A68: a,c // a',c' and
A69: b,c // b',c' and
A70: not LIN a,b,c and
A71: c <> c' ; :: thesis: A // C
assume A72: not A // C ; :: thesis: contradiction
consider K being Subset of such that
A73: c' in K and
A74: A // K by A62, AFF_1:63;
A75: a <> c by A70, AFF_1:16;
A76: not a,c // K

proof

assume a,c // K ; :: thesis: contradiction
then a,c // A by A74, AFF_1:57;
then A77: c in A by A57, A62, AFF_1:37;
a',c' // a,c by A68, AFF_1:13;
then a',c' // A by A57, A62, A75, A77, AFF_1:41;
then c' in A by A58, A62, AFF_1:37;
hence contradiction by A61, A62, A64, A66, A71, A77, AFF_1:30; :: thesis: verum

end;

A78: A <> K

proof

assume A79: A = K ; :: thesis: contradiction
a',c' // a,c by A68, AFF_1:13;
then a' = c' by A58, A73, A74, A76, A79, AFF_1:46, AFF_1:54;
then a',b' // b,c by A69, AFF_1:13;
then ( a' = b' or a,b // b,c ) by A67, AFF_1:14;
then ( b' in A or b,a // b,c ) by A58, AFF_1:13;
then LIN b,a,c by A56, A60, A65, AFF_1:59, AFF_1:def 1;
hence contradiction by A70, AFF_1:15; :: thesis: verum

end;

A80: now

assume b' = c' ; :: thesis: contradiction
then ( a,b // a,c or a' = b' ) by A67, A68, AFF_1:14;
hence contradiction by A56, A58, A60, A65, A70, AFF_1:59, AFF_1:def 1; :: thesis: verum

end;

A81: K is being_line by A74, AFF_1:50;
then consider x being Element of such that
A82: x in K and
A83: LIN a,c,x by A76, AFF_1:73;
a,c // a,x by A83, AFF_1:def 1;
then a,x // a',c' by A68, A75, AFF_1:14;
then b,x // b',c' by A55, A56, A57, A58, A59, A60, A62, A63, A65, A67, A73, A74, A81, A82, A78, Def11;
then ( b,x // b,c or b' = c' ) by A69, AFF_1:14;
then LIN b,x,c by A80, AFF_1:def 1;
then A84: LIN x,c,b by AFF_1:15;
A85: LIN x,c,c by AFF_1:16;
LIN x,c,a by A83, AFF_1:15;
then c in K by A70, A82, A84, A85, AFF_1:17;
hence contradiction by A61, A64, A71, A72, A73, A74, A81, AFF_1:30; :: thesis: verum

end;

end;

hence ( AP is translational iff AP is satisfying_des_1 ) by A1; :: thesis: verum