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

A1: now

assume A2: 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, a', b', c' being Element of AP 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 AP; :: thesis: for a, b, c, a', b', c' being Element of AP 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 AP; :: 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 A3: ( 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' ) ; :: thesis: A // C
assume A4: not A // C ; :: thesis: contradiction
A5: ( a <> b & a <> c & b <> c ) by A3, AFF_1:16;
consider K being Subset of AP such that
A6: ( c' in K & A // K ) by A3, AFF_1:63;
A7: ( K is being_line & C <> K ) by A4, A6, AFF_1:50;
A8: not a,c // K

proof

assume a,c // K ; :: thesis: contradiction
then a,c // A by A6, AFF_1:57;
then A9: c in A by A3, AFF_1:37;
a',c' // a,c by A3, AFF_1:13;
then a',c' // A by A3, A5, A9, AFF_1:41;
then c' in A by A3, AFF_1:37;
hence contradiction by A3, A9, AFF_1:30; :: thesis: verum

end;

then consider x being Element of AP such that
A10: ( x in K & LIN a,c,x ) by A7, AFF_1:73;
A11: A <> K

proof

assume A = K ; :: thesis: contradiction
then ( a',c' // K & a',c' // a,c ) by A3, A6, AFF_1:13, AFF_1:54;
then a' = c' by A8, AFF_1:46;
then ( a',b' // a,b & a',b' // b,c ) by A3, AFF_1:13;
then ( a' = b' or a,b // b,c ) by AFF_1:14;
then ( b' in A or b,a // b,c ) by A3, AFF_1:13;
then LIN b,a,c by A3, AFF_1:59, AFF_1:def 1;
hence contradiction by A3, AFF_1:15; :: thesis: verum

end;

a,c // a,x by A10, AFF_1:def 1;
then a,x // a',c' by A3, A5, AFF_1:14;
then ( b,x // b',c' & b',c' // b,c ) by A2, A3, A6, A7, A10, A11, Def11, AFF_1:13;
then A12: ( b,x // b,c or b' = c' ) by AFF_1:14;

now

assume b' = c' ; :: thesis: contradiction
then ( a,b // a,c or a' = b' ) by A3, AFF_1:14;
hence contradiction by A3, AFF_1:59, AFF_1:def 1; :: thesis: verum

end;

then LIN b,x,c by A12, AFF_1:def 1;
then ( LIN x,c,b & LIN x,c,a & LIN x,c,c ) by A10, AFF_1:15, AFF_1:16;
then c in K by A3, A10, AFF_1:17;
hence contradiction by A3, A6, A7, AFF_1:30; :: thesis: verum

end;

end;

now

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

proof

let A be Subset of AP; :: according to AFF_2:def 11 :: thesis: for P, C being Subset of AP
for a, b, c, a', b', c' being Element of AP 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 AP; :: thesis: for a, b, c, a', b', c' being Element of AP 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 AP; :: 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 A14: ( 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' ) ; :: thesis: b,c // b',c'
assume A15: not b,c // b',c' ; :: thesis: contradiction
then A16: ( b <> c & b' <> c' ) by AFF_1:12;
A17: ( a <> c & a <> b & a' <> b' & a' <> c' ) by A14, AFF_1:59;
set K = Line a,c;
set N = Line b',c';
A18: P // C by A14, AFF_1:58;
A19: ( Line a,c is being_line & Line b',c' is being_line & a in Line a,c & c in Line a,c & b' in Line b',c' & c' in Line b',c' ) by A16, A17, AFF_1:38;
then consider M being Subset of AP such that
A20: ( b in M & Line b',c' // M ) by AFF_1:63;
A21: M is being_line by A20, AFF_1:50;
A22: not LIN a,b,c

proof

assume A23: 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 A24: b,c // a',b' by A14, A17, AFF_1:14;
LIN c,b,a by A23, 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 A14, A17, AFF_1:14;
then a',c' // a',b' by A16, A24, 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 A15, A17, A24, AFF_1:14; :: thesis: verum

end;

A25: 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 A14, A17, AFF_1:14;
then a,b // a,c by A14, A17, AFF_1:14;
hence contradiction by A22, AFF_1:def 1; :: thesis: verum

end;

A26: not Line a,c // M

proof

assume Line a,c // M ; :: thesis: contradiction
then Line a,c // Line b',c' by A20, AFF_1:58;
then a,c // b',c' by A19, AFF_1:53;
then a',c' // b',c' by A14, A17, 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 A25, AFF_1:15; :: thesis: verum

end;

then consider x being Element of AP such that
A27: ( x in Line a,c & x in M ) by A19, A21, AFF_1:72;
A28: b,x // b',c' by A19, A20, A27, AFF_1:53;
A29: a,x // a',c'

proof

LIN a,c,x by A19, A27, AFF_1:33;
then a,c // a,x by AFF_1:def 1;
hence a,x // a',c' by A14, A17, AFF_1:14; :: thesis: verum

end;

set D = Line x,c';
A30: ( x in Line x,c' & c' in Line x,c' ) by AFF_1:26;
A31: x <> c'

proof

assume x = c' ; :: thesis: contradiction
then M = Line b',c' by A19, A20, A27, AFF_1:59;
then A32: ( P = Line b',c' or b = b' ) by A14, A19, A20, AFF_1:30;

A33: now

assume P = Line b',c' ; :: thesis: contradiction
then ( c' in P & c in P & P // P ) by A14, A18, A19, AFF_1:59;
hence contradiction by A14, A15, AFF_1:53; :: thesis: verum

end;

then b,a // b,a' by A14, A32, 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 A14, AFF_1:39;
then LIN a',c,c' by A14, AFF_1:59, AFF_1:def 1;
then LIN c,c',a' by AFF_1:15;
then ( c = c' or a' in C ) by A14, AFF_1:39;
hence contradiction by A14, A15, A32, A33, AFF_1:11, AFF_1:59; :: thesis: verum

end;

then A34: Line x,c' is being_line by AFF_1:38;
A35: not LIN a,b,x

proof

assume LIN a,b,x ; :: thesis: contradiction
then LIN x,b,a by AFF_1:15;
then A36: x,b // x,a by AFF_1:def 1;
A37: x <> b by A19, A22, A27, AFF_1:33;
a <> x

proof

assume a = x ; :: thesis: contradiction
then a,b // b',c' by A19, A20, A27, AFF_1:53;
then a',b' // b',c' by A14, A17, 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 A25, AFF_1:15; :: thesis: verum

end;

hence contradiction by A19, A20, A21, A26, A27, A36, A37, AFF_1:52; :: thesis: verum

end;

A <> Line x,c'

proof

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

end;

then A // Line x,c' by A13, A14, A28, A29, A30, A31, A34, A35, Def12;
then Line x,c' // C by A14, AFF_1:58;
then C = Line x,c' by A14, A30, AFF_1:59;
then C = Line a,c by A14, A15, A19, A27, A28, A30, AFF_1:30;
hence contradiction by A14, A19, AFF_1:59; :: thesis: verum

end;

end;

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