let X be OrtAfPl; :: thesis: ( AffinStruct(# the carrier of X, the CONGR of X #) is translational implies X is satisfying_des )
assume A1: AffinStruct(# the carrier of X, the CONGR of X #) is translational ; :: thesis: X is satisfying_des
let a be Element of X; :: according to CONMETR:def 8 :: thesis: for a1, b, b1, c, c1 being Element of X 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 a1, b, b1, c, c1 be Element of X; :: 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
A2: not LIN a,a1,b and
A3: not LIN a,a1,c and
A4: a,a1 // b,b1 and
A5: a,a1 // c,c1 and
A6: a,b // a1,b1 and
A7: 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 X, the CONGR of X #) ;
LIN a9,a19,a19 by AFF_1:7;
then consider A9 being Subset of AffinStruct(# the carrier of X, the CONGR of X #) such that
A8: A9 is being_line and
A9: a9 in A9 and
A10: a19 in A9 and
a19 in A9 by AFF_1:21;
A11: a9,b9 // a19,b19 by A6, ANALMETR:36;
b,b1 // a,a1 by A4, ANALMETR:59;
then A12: b9,b19 // a9,a19 by ANALMETR:36;
A13: a9 <> a19
proof
assume a9 = a19 ; :: thesis: contradiction
then LIN a9,a19,b9 by AFF_1:7;
hence contradiction by A2, ANALMETR:40; :: thesis: verum
end;
then for x9 being Element of AffinStruct(# the carrier of X, the CONGR of X #) holds
( x9 in A9 iff LIN a9,a19,x9 ) by A8, A9, A10, AFF_1:21, AFF_1:25;
then A9 = Line (a9,a19) by AFF_1:def 2;
then A14: b9,b19 // A9 by A13, A12, AFF_1:def 4;
A15: a9,c9 // a19,c19 by A7, ANALMETR:36;
c,c1 // a,a1 by A5, ANALMETR:59;
then A16: c9,c19 // a9,a19 by ANALMETR:36;
A17: a9 <> a19
proof
assume a9 = a19 ; :: thesis: contradiction
then LIN a9,a19,b9 by AFF_1:7;
hence contradiction by A2, ANALMETR:40; :: thesis: verum
end;
then for x9 being Element of AffinStruct(# the carrier of X, the CONGR of X #) holds
( x9 in A9 iff LIN a9,a19,x9 ) by A8, A9, A10, AFF_1:21, AFF_1:25;
then A9 = Line (a9,a19) by AFF_1:def 2;
then A18: c9,c19 // A9 by A17, A16, AFF_1:def 4;
LIN c9,c19,c19 by AFF_1:7;
then consider N9 being Subset of AffinStruct(# the carrier of X, the CONGR of X #) such that
A19: N9 is being_line and
A20: c9 in N9 and
A21: c19 in N9 and
c19 in N9 by AFF_1:21;
LIN b9,b19,b19 by AFF_1:7;
then consider M9 being Subset of AffinStruct(# the carrier of X, the CONGR of X #) such that
A22: M9 is being_line and
A23: b9 in M9 and
A24: b19 in M9 and
b19 in M9 by AFF_1:21;
A25: ( A9 <> M9 & A9 <> N9 )
proof
assume ( A9 = M9 or A9 = N9 ) ; :: thesis: contradiction
then ( LIN a9,a19,b9 or LIN a9,a19,c9 ) by A8, A9, A10, A23, A20, AFF_1:21;
hence contradiction by A2, A3, ANALMETR:40; :: thesis: verum
end;
A26: c9 <> c19
proof
assume c9 = c19 ; :: thesis: contradiction
then c,a // c,a1 by A7, ANALMETR:59;
then LIN c,a,a1 by ANALMETR:def 10;
then LIN c9,a9,a19 by ANALMETR:40;
then LIN a9,a19,c9 by AFF_1:6;
hence contradiction by A3, ANALMETR:40; :: thesis: verum
end;
then for x9 being Element of AffinStruct(# the carrier of X, the CONGR of X #) holds
( x9 in N9 iff LIN c9,c19,x9 ) by A19, A20, A21, AFF_1:21, AFF_1:25;
then N9 = Line (c9,c19) by AFF_1:def 2;
then A27: A9 // N9 by A18, A26, AFF_1:def 5;
A28: b9 <> b19
proof
assume b9 = b19 ; :: thesis: contradiction
then b,a // b,a1 by A6, ANALMETR:59;
then LIN b,a,a1 by ANALMETR:def 10;
then LIN b9,a9,a19 by ANALMETR:40;
then LIN a9,a19,b9 by AFF_1:6;
hence contradiction by A2, ANALMETR:40; :: thesis: verum
end;
then for x9 being Element of AffinStruct(# the carrier of X, the CONGR of X #) holds
( x9 in M9 iff LIN b9,b19,x9 ) by A22, A23, A24, AFF_1:21, AFF_1:25;
then M9 = Line (b9,b19) by AFF_1:def 2;
then A9 // M9 by A14, A28, AFF_1:def 5;
then b9,c9 // b19,c19 by A1, A8, A9, A10, A22, A23, A24, A19, A20, A21, A27, A25, A11, A15;
hence b,c // b1,c1 by ANALMETR:36; :: thesis: verum