let MS be OrtAfPl; :: thesis: ( MS is satisfying_des iff AffinStruct(# the carrier of MS, the CONGR of MS #) is translational )
set AS = AffinStruct(# the carrier of MS, the CONGR of MS #);
A1: now :: thesis: ( MS is satisfying_des implies AffinStruct(# the carrier of MS, the CONGR of MS #) is translational )
assume A2: MS is satisfying_des ; :: thesis: AffinStruct(# the carrier of MS, the CONGR of MS #) is translational
now :: thesis: for A, P, C being Subset of AffinStruct(# the carrier of MS, the CONGR of MS #)
for a, b, c, a9, b9, c9 being Element of AffinStruct(# the carrier of MS, the CONGR of MS #) 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, P, C be Subset of AffinStruct(# the carrier of MS, the CONGR of MS #); :: thesis: for a, b, c, a9, b9, c9 being Element of AffinStruct(# the carrier of MS, the CONGR of MS #) 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 AffinStruct(# the carrier of MS, the CONGR of MS #); :: 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
A3: A // P and
A4: A // C and
A5: a in A and
A6: a9 in A and
A7: b in P and
A8: b9 in P and
A9: c in C and
A10: c9 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 // a9,b9 and
A17: a,c // a9,c9 ; :: thesis: b,c // b9,c9
A18: not a in C by A4, A5, A15, AFF_1:45;
A19: now :: thesis: ( a <> a9 implies b,c // b9,c9 )
reconsider aa = a, a1 = a9, bb = b, b1 = b9, cc = c, c1 = c9 as Element of MS ;
a,a9 // b,b9 by A3, A5, A6, A7, A8, AFF_1:39;
then A20: aa,a1 // bb,b1 by ANALMETR:36;
a,a9 // c,c9 by A4, A5, A6, A9, A10, AFF_1:39;
then A21: aa,a1 // cc,c1 by ANALMETR:36;
assume A22: a <> a9 ; :: thesis: b,c // b9,c9
A23: not LIN aa,a1,bb
proof
assume LIN aa,a1,bb ; :: thesis: contradiction
then LIN a,a9,b by ANALMETR:40;
then b in A by A5, A6, A11, A22, AFF_1:25;
hence contradiction by A3, A7, A14, AFF_1:45; :: thesis: verum
end;
A24: not LIN aa,a1,cc
proof
assume LIN aa,a1,cc ; :: thesis: contradiction
then LIN a,a9,c by ANALMETR:40;
then c in A by A5, A6, A11, A22, AFF_1:25;
hence contradiction by A4, A9, A15, AFF_1:45; :: thesis: verum
end;
( aa,bb // a1,b1 & aa,cc // a1,c1 ) by A16, A17, ANALMETR:36;
then bb,cc // b1,c1 by A2, A23, A24, A20, A21, CONMETR:def 8;
hence b,c // b9,c9 by ANALMETR:36; :: thesis: verum
end;
A25: not a in P by A3, A5, A14, AFF_1:45;
now :: thesis: ( a = a9 implies b,c // b9,c9 )
assume A26: a = a9 ; :: thesis: b,c // b9,c9
then LIN a,c,c9 by A17, AFF_1:def 1;
then LIN c,c9,a by AFF_1:6;
then A27: c = c9 by A9, A10, A13, A18, AFF_1:25;
LIN a,b,b9 by A16, A26, AFF_1:def 1;
then LIN b,b9,a by AFF_1:6;
then b = b9 by A7, A8, A12, A25, AFF_1:25;
hence b,c // b9,c9 by A27, AFF_1:2; :: thesis: verum
end;
hence b,c // b9,c9 by A19; :: thesis: verum
end;
hence AffinStruct(# the carrier of MS, the CONGR of MS #) is translational by AFF_2:def 11; :: thesis: verum
end;
now :: thesis: ( AffinStruct(# the carrier of MS, the CONGR of MS #) is translational implies MS is satisfying_des )
assume A28: AffinStruct(# the carrier of MS, the CONGR of MS #) is translational ; :: thesis: MS is satisfying_des
now :: thesis: for a, a1, b, b1, c, c1 being Element of MS st not LIN a,a1,b & not LIN a,a1,c & a,a1 // b,b1 & a,a1 // c,c1 & a,b // a1,b1 & a,c // a1,c1 holds
b,c // b1,c1
let a, a1, b, b1, c, c1 be Element of MS; :: thesis: ( not LIN a,a1,b & not LIN a,a1,c & a,a1 // b,b1 & a,a1 // c,c1 & a,b // a1,b1 & a,c // a1,c1 implies b,c // b1,c1 )
assume that
A29: ( not LIN a,a1,b & not LIN a,a1,c ) and
A30: a,a1 // b,b1 and
A31: a,a1 // c,c1 and
A32: ( a,b // a1,b1 & 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 AffinStruct(# the carrier of MS, the CONGR of MS #) ;
A33: a9,a19 // b9,b19 by A30, ANALMETR:36;
A34: ( a9,b9 // a19,b19 & a9,c9 // a19,c19 ) by A32, ANALMETR:36;
A35: a9,a19 // c9,c19 by A31, ANALMETR:36;
set A = Line (a9,a19);
A36: ( not a9,a19 // a9,b9 & not a9,a19 // a9,c9 )
proof
assume ( a9,a19 // a9,b9 or a9,a19 // a9,c9 ) ; :: thesis: contradiction
then ( a,a1 // a,b or a,a1 // a,c ) by ANALMETR:36;
hence contradiction by A29, ANALMETR:def 10; :: thesis: verum
end;
then A37: a9 <> a19 by AFF_1:3;
then A38: Line (a9,a19) is being_line by AFF_1:def 3;
then consider C being Subset of AffinStruct(# the carrier of MS, the CONGR of MS #) such that
A39: c9 in C and
A40: Line (a9,a19) // C by AFF_1:49;
A41: C is being_line by A40, AFF_1:36;
A42: ( a9 in Line (a9,a19) & a19 in Line (a9,a19) ) by AFF_1:15;
then A43: Line (a9,a19) <> C by A36, A38, A39, AFF_1:51;
A44: a9,a19 // Line (a9,a19) by A38, A42, AFF_1:23;
then a9,a19 // C by A40, AFF_1:43;
then c9,c19 // C by A35, A37, AFF_1:32;
then A45: c19 in C by A39, A41, AFF_1:23;
consider P being Subset of AffinStruct(# the carrier of MS, the CONGR of MS #) such that
A46: b9 in P and
A47: Line (a9,a19) // P by A38, AFF_1:49;
A48: P is being_line by A47, AFF_1:36;
a9,a19 // P by A44, A47, AFF_1:43;
then b9,b19 // P by A33, A37, AFF_1:32;
then A49: b19 in P by A46, A48, AFF_1:23;
Line (a9,a19) <> P by A36, A38, A42, A46, AFF_1:51;
then b9,c9 // b19,c19 by A28, A34, A38, A42, A46, A47, A39, A40, A48, A41, A49, A45, A43, AFF_2:def 11;
hence b,c // b1,c1 by ANALMETR:36; :: thesis: verum
end;
hence MS is satisfying_des by CONMETR:def 8; :: thesis: verum
end;
hence ( MS is satisfying_des iff AffinStruct(# the carrier of MS, the CONGR of MS #) is translational ) by A1; :: thesis: verum