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

( 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

( 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 )

( 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

( 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

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

then
for x9 being Element of AffinStruct(# the carrier of X, the CONGR of X #) holds
assume
a9 = a19
; :: thesis: contradiction

then LIN a9,a19,b9 by AFF_1:7;

hence contradiction by A2, ANALMETR:40; :: thesis: verum

end;then LIN a9,a19,b9 by AFF_1:7;

hence contradiction by A2, ANALMETR:40; :: thesis: verum

( 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

then
for x9 being Element of AffinStruct(# the carrier of X, the CONGR of X #) holds
assume
a9 = a19
; :: thesis: contradiction

then LIN a9,a19,b9 by AFF_1:7;

hence contradiction by A2, ANALMETR:40; :: thesis: verum

end;then LIN a9,a19,b9 by AFF_1:7;

hence contradiction by A2, ANALMETR:40; :: thesis: verum

( 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

A26:
c9 <> c19
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;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

proof

then
for x9 being Element of AffinStruct(# the carrier of X, the CONGR of X #) holds
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 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

( 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

then
for x9 being Element of AffinStruct(# the carrier of X, the CONGR of X #) holds
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 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

( 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