let X be OrtAfPl; :: thesis: ( AffinStruct(# the U1 of X, the CONGR of X #) is translational iff X is satisfying_des )
( X is satisfying_des implies AffinStruct(# the U1 of X, the CONGR of X #) is translational )

proof

assume A1: X is satisfying_des ; :: thesis: AffinStruct(# the U1 of X, the CONGR of X #) is translational

now :: thesis: for A, M, N being Subset of AffinStruct(# the U1 of X, the CONGR of X #)
for a, b, c, a1, b1, c1 being Element of AffinStruct(# the U1 of X, the CONGR of X #) st A // M & A // N & a in A & a1 in A & b in M & b1 in M & c in N & c1 in N & A is being_line & M is being_line & N is being_line & A <> M & A <> N & a,b // a1,b1 & a,c // a1,c1 holds
b,c // b1,c1

let A, M, N be Subset of AffinStruct(# the U1 of X, the CONGR of X #); :: thesis: for a, b, c, a1, b1, c1 being Element of AffinStruct(# the U1 of X, the CONGR of X #) st A // M & A // N & a in A & a1 in A & b in M & b1 in M & c in N & c1 in N & A is being_line & M is being_line & N is being_line & A <> M & A <> N & a,b // a1,b1 & a,c // a1,c1 holds
b,c // b1,c1
let a, b, c, a1, b1, c1 be Element of AffinStruct(# the U1 of X, the CONGR of X #); :: thesis: ( A // M & A // N & a in A & a1 in A & b in M & b1 in M & c in N & c1 in N & A is being_line & M is being_line & N is being_line & A <> M & A <> N & a,b // a1,b1 & a,c // a1,c1 implies b,c // b1,c1 )
assume that
A2: A // M and
A3: A // N and
A4: a in A and
A5: a1 in A and
A6: b in M and
A7: b1 in M and
A8: c in N and
A9: c1 in N and
A10: A is being_line and
A11: M is being_line and
A12: N is being_line and
A13: A <> M and
A14: A <> N and
A15: a,b // a1,b1 and
A16: a,c // a1,c1 ; :: thesis: b,c // b1,c1
reconsider a9 = a, a19 = a1, b9 = b, b19 = b1, c9 = c, c19 = c1 as Element of X ;
b,c // b1,c1

proof

assume A17: not b,c // b1,c1 ; :: thesis: contradiction
A18: a <> a1

proof

assume A19: a = a1 ; :: thesis: contradiction
A20: c = c1

proof

LIN a,c,c1 by A16, A19, AFF_1:def 1;
then A21: LIN c,c1,a by AFF_1:6;
assume c <> c1 ; :: thesis: contradiction
then a in N by A8, A9, A12, A21, AFF_1:25;
hence contradiction by A3, A4, A14, AFF_1:45; :: thesis: verum

end;

b = b1

proof

LIN a,b,b1 by A15, A19, AFF_1:def 1;
then A22: LIN b,b1,a by AFF_1:6;
assume b <> b1 ; :: thesis: contradiction
then a in M by A6, A7, A11, A22, AFF_1:25;
hence contradiction by A2, A4, A13, AFF_1:45; :: thesis: verum

end;

hence contradiction by A17, A20, AFF_1:2; :: thesis: verum

end;

A23: ( not LIN a9,a19,b9 & not LIN a9,a19,c9 )

proof

assume ( LIN a9,a19,b9 or LIN a9,a19,c9 ) ; :: thesis: contradiction
then ( LIN a,a1,b or LIN a,a1,c ) by ANALMETR:40;
then ( b in A or c in A ) by A4, A5, A10, A18, AFF_1:25;
hence contradiction by A2, A3, A6, A8, A13, A14, AFF_1:45; :: thesis: verum

end;

a,a1 // c,c1 by A3, A4, A5, A8, A9, AFF_1:39;
then A24: a9,a19 // c9,c19 by ANALMETR:36;
a,a1 // b,b1 by A2, A4, A5, A6, A7, AFF_1:39;
then A25: a9,a19 // b9,b19 by ANALMETR:36;
A26: a9,c9 // a19,c19 by A16, ANALMETR:36;
a9,b9 // a19,b19 by A15, ANALMETR:36;
then b9,c9 // b19,c19 by A1, A23, A25, A24, A26, CONMETR:def 8;
hence contradiction by A17, ANALMETR:36; :: thesis: verum

end;

hence b,c // b1,c1 ; :: thesis: verum

end;

hence AffinStruct(# the U1 of X, the CONGR of X #) is translational by AFF_2:def 11; :: thesis: verum

end;

hence ( AffinStruct(# the U1 of X, the CONGR of X #) is translational iff X is satisfying_des ) by CONMETR:8; :: thesis: verum