:: HOMOTHET semantic presentation

Lemma1: for b₁ being AffinPlane holds
( b₁ satisfies_DES iff for b₂, b₃, b₄, b₅, b₆, b₇, b₈ being Element of b₁ st LIN b₂,b₃,b₄ & LIN b₂,b₅,b₆ & LIN b₂,b₇,b₈ & not LIN b₂,b₃,b₅ & not LIN b₂,b₃,b₇ & b₃,b₅ // b₄,b₆ & b₃,b₇ // b₄,b₈ holds
b₅,b₇ // b₆,b₈ )

proof end;

Lemma2: for b₁ being AffinPlane holds
( b₁ satisfies_TDES iff for b₂ being Element of b₁
for b₃ being Subset of b₁
for b₄, b₅, b₆, b₇, b₈, b₉ being Element of b₁ st b₂ in b₃ & b₄ in b₃ & b₅ in b₃ & b₃ is_line & LIN b₂,b₆,b₈ & LIN b₂,b₇,b₉ & not b₆ in b₃ & b₆,b₇ // b₃ & b₈,b₉ // b₃ & b₆,b₄ // b₈,b₅ holds
b₇,b₄ // b₉,b₅ )

proof end;

Lemma3: for b₁ being AffinPlane st b₁ satisfies_TDES holds
for b₂ being Subset of b₁
for b₃, b₄, b₅, b₆, b₇, b₈, b₉ being Element of b₁ st b₂ is_line & b₃ in b₂ & b₆ in b₂ & b₉ in b₂ & not b₄ in b₂ & b₄ <> b₅ & LIN b₃,b₄,b₇ & b₄,b₅ // b₇,b₈ & b₅,b₆ // b₈,b₉ & b₄,b₆ // b₇,b₉ & b₄,b₅ // b₂ holds
LIN b₃,b₅,b₈

proof end;

Lemma4: for b₁ being AffinPlane st b₁ satisfies_TDES holds
for b₂, b₃, b₄ being Subset of b₁
for b₅, b₆, b₇, b₈, b₉, b₁₀ being Element of b₁ st b₂ // b₃ & b₂ // b₄ & b₂ <> b₃ & b₂ <> b₄ & b₅ in b₂ & b₆ in b₂ & b₇ in b₃ & b₈ in b₃ & b₉ in b₄ & b₁₀ in b₄ & b₅,b₇ // b₆,b₈ & b₅,b₉ // b₆,b₁₀ holds
b₇,b₉ // b₈,b₁₀

proof end;

theorem Th1: :: HOMOTHET:1

for b₁ being AffinPlane
for b₂, b₃, b₄, b₅, b₆, b₇, b₈, b₉, b₁₀ being Element of b₁ st not LIN b₂,b₃,b₄ & LIN b₂,b₃,b₅ & LIN b₂,b₃,b₆ & LIN b₂,b₃,b₇ & LIN b₂,b₄,b₈ & LIN b₂,b₄,b₉ & LIN b₂,b₄,b₁₀ & b₄ <> b₉ & b₃ <> b₆ & b₂ <> b₉ & b₂ <> b₆ & b₃,b₄ // b₅,b₈ & b₃,b₉ // b₅,b₁₀ & b₆,b₄ // b₇,b₈ & b₁ satisfies_DES holds
b₆,b₉ // b₇,b₁₀

proof end;

theorem Th2: :: HOMOTHET:2

for b₁ being AffinPlane st ( for b₂, b₃, b₄ being Element of b₁ st b₂ <> b₃ & b₂ <> b₄ & LIN b₂,b₃,b₄ holds
ex b₅ being Permutation of the carrier of b₁ st
( b₅ is_Dil & b₅ . b₂ = b₂ & b₅ . b₃ = b₄ ) ) holds
b₁ satisfies_DES

proof end;

Lemma7: for b₁ being AffinPlane
for b₂, b₃, b₄, b₅, b₆ being Element of b₁ st b₂ <> b₃ & b₂ <> b₄ & LIN b₂,b₃,b₄ & LIN b₂,b₃,b₅ & ( ( not LIN b₂,b₃,b₆ & LIN b₂,b₆,b₅ & b₃,b₆ // b₄,b₅ ) or ( LIN b₂,b₃,b₆ & ex b₇, b₈ being Element of b₁ st
( not LIN b₂,b₃,b₇ & LIN b₂,b₇,b₈ & b₃,b₇ // b₄,b₈ & b₇,b₆ // b₈,b₅ & LIN b₂,b₃,b₅ ) ) ) holds
LIN b₂,b₃,b₆

proof end;

Lemma8: for b₁ being AffinPlane
for b₂, b₃, b₄, b₅, b₆ being Element of b₁ st b₂ <> b₃ & b₂ <> b₄ & LIN b₂,b₃,b₄ & ( ( not LIN b₂,b₃,b₅ & LIN b₂,b₅,b₆ & b₃,b₅ // b₄,b₆ ) or ( LIN b₂,b₃,b₅ & ex b₇, b₈ being Element of b₁ st
( not LIN b₂,b₃,b₇ & LIN b₂,b₇,b₈ & b₃,b₇ // b₄,b₈ & b₇,b₅ // b₈,b₆ & LIN b₂,b₃,b₆ ) ) ) holds
( b₂ <> b₄ & b₂ <> b₃ & LIN b₂,b₄,b₃ & ( ( not LIN b₂,b₄,b₆ & LIN b₂,b₆,b₅ & b₄,b₆ // b₃,b₅ ) or ( LIN b₂,b₄,b₆ & ex b₇, b₈ being Element of b₁ st
( not LIN b₂,b₄,b₇ & LIN b₂,b₇,b₈ & b₄,b₇ // b₃,b₈ & b₇,b₆ // b₈,b₅ & LIN b₂,b₄,b₅ ) ) ) )

proof end;

Lemma9: for b₁ being AffinPlane
for b₂, b₃, b₄, b₅, b₆ being Element of b₁ st b₂ <> b₃ & b₂ <> b₄ & LIN b₂,b₃,b₄ & b₅ = b₂ & ( ( not LIN b₂,b₃,b₅ & LIN b₂,b₅,b₆ & b₃,b₅ // b₄,b₆ ) or ( LIN b₂,b₃,b₅ & ex b₇, b₈ being Element of b₁ st
( not LIN b₂,b₃,b₇ & LIN b₂,b₇,b₈ & b₃,b₇ // b₄,b₈ & b₇,b₅ // b₈,b₆ & LIN b₂,b₃,b₆ ) ) ) holds
b₆ = b₂

proof end;

Lemma10: for b₁ being AffinPlane
for b₂, b₃, b₄, b₅ being Element of b₁ st b₂ <> b₃ & b₂ <> b₄ & LIN b₂,b₃,b₄ holds
ex b₆ being Element of b₁ st
( ( not LIN b₂,b₃,b₅ & LIN b₂,b₅,b₆ & b₃,b₅ // b₄,b₆ ) or ( LIN b₂,b₃,b₅ & ex b₇, b₈ being Element of b₁ st
( not LIN b₂,b₃,b₇ & LIN b₂,b₇,b₈ & b₃,b₇ // b₄,b₈ & b₇,b₅ // b₈,b₆ & LIN b₂,b₃,b₆ ) ) )

proof end;

Lemma11: for b₁ being AffinPlane
for b₂, b₃, b₄, b₅ being Element of b₁ st b₂ <> b₃ & b₂ <> b₄ & LIN b₂,b₃,b₄ holds
ex b₆ being Element of b₁ st
( ( not LIN b₂,b₃,b₆ & LIN b₂,b₆,b₅ & b₃,b₆ // b₄,b₅ ) or ( LIN b₂,b₃,b₆ & ex b₇, b₈ being Element of b₁ st
( not LIN b₂,b₃,b₇ & LIN b₂,b₇,b₈ & b₃,b₇ // b₄,b₈ & b₇,b₆ // b₈,b₅ & LIN b₂,b₃,b₅ ) ) )

proof end;

Lemma12: for b₁ being AffinPlane
for b₂, b₃, b₄, b₅, b₆ being Element of b₁ st b₂ <> b₃ & b₂ <> b₄ & LIN b₂,b₃,b₄ & b₃ = b₄ & ( ( not LIN b₂,b₃,b₅ & LIN b₂,b₅,b₆ & b₃,b₅ // b₄,b₆ ) or ( LIN b₂,b₃,b₅ & ex b₇, b₈ being Element of b₁ st
( not LIN b₂,b₃,b₇ & LIN b₂,b₇,b₈ & b₃,b₇ // b₄,b₈ & b₇,b₅ // b₈,b₆ & LIN b₂,b₃,b₆ ) ) ) holds
b₅ = b₆

proof end;

Lemma13: for b₁ being AffinPlane
for b₂, b₃, b₄, b₅, b₆, b₇ being Element of b₁ st b₂ <> b₃ & b₂ <> b₄ & LIN b₂,b₃,b₄ & b₁ satisfies_DES & LIN b₂,b₃,b₅ & ex b₈, b₉ being Element of b₁ st
( not LIN b₂,b₃,b₈ & LIN b₂,b₈,b₉ & b₃,b₈ // b₄,b₉ & b₈,b₅ // b₉,b₆ & LIN b₂,b₃,b₆ ) & ex b₈, b₉ being Element of b₁ st
( not LIN b₂,b₃,b₈ & LIN b₂,b₈,b₉ & b₃,b₈ // b₄,b₉ & b₈,b₅ // b₉,b₇ & LIN b₂,b₃,b₇ ) holds
b₆ = b₇

proof end;

Lemma14: for b₁ being AffinPlane
for b₂, b₃, b₄, b₅, b₆, b₇ being Element of b₁ st b₂ <> b₃ & b₂ <> b₄ & LIN b₂,b₃,b₄ & b₁ satisfies_DES & ( ( not LIN b₂,b₃,b₅ & LIN b₂,b₅,b₆ & b₃,b₅ // b₄,b₆ ) or ( LIN b₂,b₃,b₅ & ex b₈, b₉ being Element of b₁ st
( not LIN b₂,b₃,b₈ & LIN b₂,b₈,b₉ & b₃,b₈ // b₄,b₉ & b₈,b₅ // b₉,b₆ & LIN b₂,b₃,b₆ ) ) ) & ( ( not LIN b₂,b₃,b₇ & LIN b₂,b₇,b₆ & b₃,b₇ // b₄,b₆ ) or ( LIN b₂,b₃,b₇ & ex b₈, b₉ being Element of b₁ st
( not LIN b₂,b₃,b₈ & LIN b₂,b₈,b₉ & b₃,b₈ // b₄,b₉ & b₈,b₇ // b₉,b₆ & LIN b₂,b₃,b₆ ) ) ) holds
b₅ = b₇

proof end;

Lemma15: for b₁ being AffinPlane
for b₂, b₃, b₄ being Element of b₁ st b₁ satisfies_DES & b₂ <> b₃ & b₂ <> b₄ & LIN b₂,b₃,b₄ holds
ex b₅ being Permutation of the carrier of b₁ st
for b₆, b₇ being Element of b₁ holds
( b₅ . b₆ = b₇ iff ( ( not LIN b₂,b₃,b₆ & LIN b₂,b₆,b₇ & b₃,b₆ // b₄,b₇ ) or ( LIN b₂,b₃,b₆ & ex b₈, b₉ being Element of b₁ st
( not LIN b₂,b₃,b₈ & LIN b₂,b₈,b₉ & b₃,b₈ // b₄,b₉ & b₈,b₆ // b₉,b₇ & LIN b₂,b₃,b₇ ) ) ) )

proof end;

Lemma16: for b₁ being AffinPlane
for b₂, b₃, b₄, b₅, b₆, b₇, b₈ being Element of b₁ st b₁ satisfies_DES & b₂ <> b₃ & b₂ <> b₄ & LIN b₂,b₃,b₄ & not LIN b₂,b₃,b₅ & LIN b₂,b₅,b₆ & b₃,b₅ // b₄,b₆ & LIN b₂,b₃,b₇ & ex b₉, b₁₀ being Element of b₁ st
( not LIN b₂,b₃,b₉ & LIN b₂,b₉,b₁₀ & b₃,b₉ // b₄,b₁₀ & b₉,b₇ // b₁₀,b₈ & LIN b₂,b₃,b₈ ) holds
b₅,b₇ // b₆,b₈

proof end;

Lemma17: for b₁ being AffinPlane
for b₂, b₃, b₄, b₅, b₆, b₇, b₈ being Element of b₁ st b₁ satisfies_DES & b₂ <> b₃ & b₂ <> b₄ & LIN b₂,b₃,b₄ & LIN b₂,b₃,b₅ & ex b₉, b₁₀ being Element of b₁ st
( not LIN b₂,b₃,b₉ & LIN b₂,b₉,b₁₀ & b₃,b₉ // b₄,b₁₀ & b₉,b₅ // b₁₀,b₆ & LIN b₂,b₃,b₆ ) & not LIN b₂,b₃,b₇ & LIN b₂,b₇,b₈ & b₃,b₇ // b₄,b₈ holds
b₅,b₇ // b₆,b₈

proof end;

Lemma18: for b₁ being AffinPlane
for b₂, b₃, b₄, b₅, b₆, b₇, b₈ being Element of b₁ st b₂ <> b₃ & b₂ <> b₄ & LIN b₂,b₃,b₄ & LIN b₂,b₃,b₅ & ex b₉, b₁₀ being Element of b₁ st
( not LIN b₂,b₃,b₉ & LIN b₂,b₉,b₁₀ & b₃,b₉ // b₄,b₁₀ & b₉,b₅ // b₁₀,b₆ & LIN b₂,b₃,b₆ ) & LIN b₂,b₃,b₇ & ex b₉, b₁₀ being Element of b₁ st
( not LIN b₂,b₃,b₉ & LIN b₂,b₉,b₁₀ & b₃,b₉ // b₄,b₁₀ & b₉,b₇ // b₁₀,b₈ & LIN b₂,b₃,b₈ ) holds
b₅,b₇ // b₆,b₈

proof end;

Lemma19: for b₁ being AffinPlane
for b₂, b₃, b₄ being Element of b₁
for b₅ being Permutation of the carrier of b₁ st b₂ <> b₃ & b₂ <> b₄ & LIN b₂,b₃,b₄ & b₁ satisfies_DES & ( for b₆, b₇ being Element of b₁ holds
( b₅ . b₆ = b₇ iff ( ( not LIN b₂,b₃,b₆ & LIN b₂,b₆,b₇ & b₃,b₆ // b₄,b₇ ) or ( LIN b₂,b₃,b₆ & ex b₈, b₉ being Element of b₁ st
( not LIN b₂,b₃,b₈ & LIN b₂,b₈,b₉ & b₃,b₈ // b₄,b₉ & b₈,b₆ // b₉,b₇ & LIN b₂,b₃,b₇ ) ) ) ) ) holds
( b₅ is_Dil & b₅ . b₂ = b₂ & b₅ . b₃ = b₄ )

proof end;

theorem Th3: :: HOMOTHET:3

for b₁ being AffinPlane st b₁ satisfies_DES holds
for b₂, b₃, b₄ being Element of b₁ st b₂ <> b₃ & b₂ <> b₄ & LIN b₂,b₃,b₄ holds
ex b₅ being Permutation of the carrier of b₁ st
( b₅ is_Dil & b₅ . b₂ = b₂ & b₅ . b₃ = b₄ )

proof end;

theorem Th4: :: HOMOTHET:4

for b₁ being AffinPlane holds
( b₁ satisfies_DES iff for b₂, b₃, b₄ being Element of b₁ st b₂ <> b₃ & b₂ <> b₄ & LIN b₂,b₃,b₄ holds
ex b₅ being Permutation of the carrier of b₁ st
( b₅ is_Dil & b₅ . b₂ = b₂ & b₅ . b₃ = b₄ ) ) by Th2, Th3;

definition

let c₁ be AffinPlane;
let c₂ be Permutation of the carrier of c₁;
let c₃ be Subset of c₁;
pred c₂ is_Sc c₃ means :Def1: :: HOMOTHET:def 1
( a₂ is_Col & a₃ is_line & ( for b₁ being Element of a₁ st b₁ in a₃ holds
a₂ . b₁ = b₁ ) & ( for b₁ being Element of a₁ holds b₁,a₂ . b₁ // a₃ ) );

end;

:: deftheorem Def1 defines is_Sc HOMOTHET:def 1 :

theorem Th5: :: HOMOTHET:5

for b₁ being AffinPlane
for b₂ being Element of b₁
for b₃ being Subset of b₁
for b₄ being Permutation of the carrier of b₁ st b₄ is_Sc b₃ & b₄ . b₂ = b₂ & not b₂ in b₃ holds
b₄ = id the carrier of b₁

proof end;

theorem Th6: :: HOMOTHET:6

for b₁ being AffinPlane st ( for b₂, b₃ being Element of b₁
for b₄ being Subset of b₁ st b₂,b₃ // b₄ & not b₂ in b₄ holds
ex b₅ being Permutation of the carrier of b₁ st
( b₅ is_Sc b₄ & b₅ . b₂ = b₃ ) ) holds
b₁ satisfies_TDES

proof end;

Lemma24: for b₁ being AffinPlane
for b₂, b₃, b₄, b₅ being Element of b₁
for b₆ being Subset of b₁ st b₂,b₃ // b₆ & not b₂ in b₆ & ( ( b₄ in b₆ & b₄ = b₅ ) or ( not b₄ in b₆ & ex b₇, b₈ being Element of b₁ st
( b₇ in b₆ & b₈ in b₆ & b₇,b₂ // b₈,b₄ & b₇,b₃ // b₈,b₅ & b₄,b₅ // b₆ ) ) ) holds
( b₃,b₂ // b₆ & not b₃ in b₆ & ( ( b₅ in b₆ & b₅ = b₄ ) or ( not b₅ in b₆ & ex b₇, b₈ being Element of b₁ st
( b₇ in b₆ & b₈ in b₆ & b₇,b₃ // b₈,b₅ & b₇,b₂ // b₈,b₄ & b₅,b₄ // b₆ ) ) ) )

proof end;

Lemma25: for b₁ being AffinPlane
for b₂, b₃ being Element of b₁
for b₄ being Subset of b₁ st b₂,b₃ // b₄ & not b₂ in b₄ holds
for b₅ being Element of b₁ ex b₆ being Element of b₁ st
( ( b₅ in b₄ & b₅ = b₆ ) or ( not b₅ in b₄ & ex b₇, b₈ being Element of b₁ st
( b₇ in b₄ & b₈ in b₄ & b₇,b₂ // b₈,b₅ & b₇,b₃ // b₈,b₆ & b₅,b₆ // b₄ ) ) )

proof end;

Lemma26: for b₁ being AffinPlane
for b₂, b₃ being Element of b₁
for b₄ being Subset of b₁ st b₂,b₃ // b₄ & not b₂ in b₄ holds
for b₅ being Element of b₁ ex b₆ being Element of b₁ st
( ( b₆ in b₄ & b₆ = b₅ ) or ( not b₆ in b₄ & ex b₇, b₈ being Element of b₁ st
( b₇ in b₄ & b₈ in b₄ & b₇,b₂ // b₈,b₆ & b₇,b₃ // b₈,b₅ & b₆,b₅ // b₄ ) ) )

proof end;

theorem Th7: :: HOMOTHET:7

for b₁ being AffinPlane
for b₂, b₃, b₄, b₅, b₆, b₇, b₈, b₉ being Element of b₁
for b₁₀, b₁₁ being Subset of b₁ st b₁₀ // b₁₁ & b₂ in b₁₀ & b₃ in b₁₀ & b₄ in b₁₀ & b₅ in b₁₀ & b₁ satisfies_TDES & b₆ in b₁₁ & b₇ in b₁₁ & b₈ in b₁₁ & b₉ in b₁₁ & b₆ <> b₇ & b₃ <> b₂ & b₂,b₆ // b₄,b₈ & b₂,b₇ // b₄,b₉ & b₃,b₆ // b₅,b₈ holds
b₃,b₇ // b₅,b₉

proof end;

Lemma28: for b₁ being AffinPlane
for b₂, b₃, b₄, b₅, b₆, b₇, b₈, b₉ being Element of b₁
for b₁₀ being Subset of b₁ st b₂,b₃ // b₁₀ & not b₂ in b₁₀ & not b₄ in b₁₀ & b₁ satisfies_TDES & b₅ in b₁₀ & b₆ in b₁₀ & b₅,b₂ // b₆,b₄ & b₅,b₃ // b₆,b₇ & b₄,b₇ // b₁₀ & b₈ in b₁₀ & b₉ in b₁₀ & b₈,b₂ // b₉,b₄ holds
b₈,b₃ // b₉,b₇

proof end;

Lemma29: for b₁ being AffinPlane
for b₂, b₃, b₄, b₅, b₆, b₇, b₈, b₉, b₁₀ being Element of b₁
for b₁₁ being Subset of b₁ st b₂,b₃ // b₁₁ & not b₂ in b₁₁ & not b₄ in b₁₁ & b₁ satisfies_TDES & b₅ in b₁₁ & b₆ in b₁₁ & b₅,b₂ // b₆,b₄ & b₅,b₃ // b₆,b₇ & b₄,b₇ // b₁₁ & b₈ in b₁₁ & b₉ in b₁₁ & b₈,b₂ // b₉,b₄ & b₄,b₁₀ // b₁₁ & b₈,b₃ // b₉,b₁₀ holds
b₁₀ = b₇

proof end;

Lemma30: for b₁ being AffinPlane
for b₂, b₃, b₄, b₅, b₆ being Element of b₁
for b₇ being Subset of b₁ st b₂,b₃ // b₇ & not b₂ in b₇ & b₁ satisfies_TDES & ( ( b₄ in b₇ & b₄ = b₅ ) or ( not b₄ in b₇ & ex b₈, b₉ being Element of b₁ st
( b₈ in b₇ & b₉ in b₇ & b₈,b₂ // b₉,b₄ & b₈,b₃ // b₉,b₅ & b₄,b₅ // b₇ ) ) ) & ( ( b₆ in b₇ & b₆ = b₅ ) or ( not b₆ in b₇ & ex b₈, b₉ being Element of b₁ st
( b₈ in b₇ & b₉ in b₇ & b₈,b₂ // b₉,b₆ & b₈,b₃ // b₉,b₅ & b₆,b₅ // b₇ ) ) ) holds
b₄ = b₆

proof end;

Lemma31: for b₁ being AffinPlane
for b₂, b₃ being Element of b₁
for b₄ being Subset of b₁ st b₂,b₃ // b₄ & not b₂ in b₄ & b₁ satisfies_TDES holds
ex b₅ being Permutation of the carrier of b₁ st
for b₆, b₇ being Element of b₁ holds
( b₅ . b₆ = b₇ iff ( ( b₆ in b₄ & b₆ = b₇ ) or ( not b₆ in b₄ & ex b₈, b₉ being Element of b₁ st
( b₈ in b₄ & b₉ in b₄ & b₈,b₂ // b₉,b₆ & b₈,b₃ // b₉,b₇ & b₆,b₇ // b₄ ) ) ) )

proof end;

Lemma32: for b₁ being AffinPlane
for b₂, b₃ being Element of b₁
for b₄ being Subset of b₁
for b₅ being Permutation of the carrier of b₁ st b₂,b₃ // b₄ & not b₂ in b₄ & ( for b₆, b₇ being Element of b₁ holds
( b₅ . b₆ = b₇ iff ( ( b₆ in b₄ & b₆ = b₇ ) or ( not b₆ in b₄ & ex b₈, b₉ being Element of b₁ st
( b₈ in b₄ & b₉ in b₄ & b₈,b₂ // b₉,b₆ & b₈,b₃ // b₉,b₇ & b₆,b₇ // b₄ ) ) ) ) ) holds
b₅ . b₂ = b₃

proof end;

Lemma33: for b₁ being AffinPlane
for b₂, b₃ being Element of b₁
for b₄ being Subset of b₁
for b₅ being Permutation of the carrier of b₁ st b₂,b₃ // b₄ & not b₂ in b₄ & ( for b₆, b₇ being Element of b₁ holds
( b₅ . b₆ = b₇ iff ( ( b₆ in b₄ & b₆ = b₇ ) or ( not b₆ in b₄ & ex b₈, b₉ being Element of b₁ st
( b₈ in b₄ & b₉ in b₄ & b₈,b₂ // b₉,b₆ & b₈,b₃ // b₉,b₇ & b₆,b₇ // b₄ ) ) ) ) ) holds
for b₆ being Element of b₁ holds b₆,b₅ . b₆ // b₄

proof end;

Lemma34: for b₁ being AffinPlane
for b₂, b₃ being Element of b₁
for b₄ being Subset of b₁
for b₅ being Permutation of the carrier of b₁ st b₂,b₃ // b₄ & not b₂ in b₄ & b₁ satisfies_TDES & ( for b₆, b₇ being Element of b₁ holds
( b₅ . b₆ = b₇ iff ( ( b₆ in b₄ & b₆ = b₇ ) or ( not b₆ in b₄ & ex b₈, b₉ being Element of b₁ st
( b₈ in b₄ & b₉ in b₄ & b₈,b₂ // b₉,b₆ & b₈,b₃ // b₉,b₇ & b₆,b₇ // b₄ ) ) ) ) ) holds
b₅ is_Col

proof end;

Lemma35: for b₁ being AffinPlane
for b₂, b₃ being Element of b₁
for b₄ being Subset of b₁
for b₅ being Permutation of the carrier of b₁ st b₂,b₃ // b₄ & not b₂ in b₄ & b₁ satisfies_TDES & ( for b₆, b₇ being Element of b₁ holds
( b₅ . b₆ = b₇ iff ( ( b₆ in b₄ & b₆ = b₇ ) or ( not b₆ in b₄ & ex b₈, b₉ being Element of b₁ st
( b₈ in b₄ & b₉ in b₄ & b₈,b₂ // b₉,b₆ & b₈,b₃ // b₉,b₇ & b₆,b₇ // b₄ ) ) ) ) ) holds
b₅ is_Sc b₄

proof end;

theorem Th8: :: HOMOTHET:8

for b₁ being AffinPlane
for b₂, b₃ being Element of b₁
for b₄ being Subset of b₁ st b₂,b₃ // b₄ & not b₂ in b₄ & b₁ satisfies_TDES holds
ex b₅ being Permutation of the carrier of b₁ st
( b₅ is_Sc b₄ & b₅ . b₂ = b₃ )

proof end;

theorem Th9: :: HOMOTHET:9

for b₁ being AffinPlane holds
( b₁ satisfies_TDES iff for b₂, b₃ being Element of b₁
for b₄ being Subset of b₁ st b₂,b₃ // b₄ & not b₂ in b₄ holds
ex b₅ being Permutation of the carrier of b₁ st
( b₅ is_Sc b₄ & b₅ . b₂ = b₃ ) ) by Th6, Th8;