:: HOMOTHET semantic presentation

begin

theorem :: HOMOTHET:1
for AFP being ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane)
for o, a, p, b, x, y, p9, q, q9 being ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) st not LIN o : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) & LIN o : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) & LIN o : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) & LIN o : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) & LIN o : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) ,p9 : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) & LIN o : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) & LIN o : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) ,q9 : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) & p : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) <> q : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) & o : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) <> q : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) & o : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) <> x : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) // b : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) ,p9 : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) // b : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) ,q9 : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) & x : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) // y : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) ,p9 : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) & AFP : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) is Desarguesian holds
x : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) // y : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) ,q9 : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) ;

theorem :: HOMOTHET:2
for AFP being ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) st ( for o, a, b being ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) st o : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) <> a : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) & o : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) <> b : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) & LIN o : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) holds
ex f being ( ( V6() quasi_total bijective ) ( V6() quasi_total bijective ) Permutation of the carrier of AFP : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V11() V12() ) set ) ) st
( f : ( ( V6() quasi_total bijective ) ( V6() quasi_total bijective ) Permutation of the carrier of b1 : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V11() V12() ) set ) ) is dilatation & f : ( ( V6() quasi_total bijective ) ( V6() quasi_total bijective ) Permutation of the carrier of b1 : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V11() V12() ) set ) ) . o : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V11() V12() ) set ) )) = o : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) & f : ( ( V6() quasi_total bijective ) ( V6() quasi_total bijective ) Permutation of the carrier of b1 : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V11() V12() ) set ) ) . a : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V11() V12() ) set ) )) = b : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) ) ) holds
AFP : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) is Desarguesian ;

theorem :: HOMOTHET:3
for AFP being ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) st AFP : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) is Desarguesian holds
for o, a, b being ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) st o : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) <> a : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) & o : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) <> b : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) & LIN o : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) holds
ex f being ( ( V6() quasi_total bijective ) ( V6() quasi_total bijective ) Permutation of the carrier of AFP : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V11() V12() ) set ) ) st
( f : ( ( V6() quasi_total bijective ) ( V6() quasi_total bijective ) Permutation of the carrier of b1 : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V11() V12() ) set ) ) is dilatation & f : ( ( V6() quasi_total bijective ) ( V6() quasi_total bijective ) Permutation of the carrier of b1 : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V11() V12() ) set ) ) . o : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V11() V12() ) set ) )) = o : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) & f : ( ( V6() quasi_total bijective ) ( V6() quasi_total bijective ) Permutation of the carrier of b1 : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V11() V12() ) set ) ) . a : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V11() V12() ) set ) )) = b : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) ) ;

theorem :: HOMOTHET:4
for AFP being ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) holds
( AFP : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) is Desarguesian iff for o, a, b being ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) st o : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) <> a : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) & o : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) <> b : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) & LIN o : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) holds
ex f being ( ( V6() quasi_total bijective ) ( V6() quasi_total bijective ) Permutation of the carrier of AFP : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V11() V12() ) set ) ) st
( f : ( ( V6() quasi_total bijective ) ( V6() quasi_total bijective ) Permutation of the carrier of b1 : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V11() V12() ) set ) ) is dilatation & f : ( ( V6() quasi_total bijective ) ( V6() quasi_total bijective ) Permutation of the carrier of b1 : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V11() V12() ) set ) ) . o : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V11() V12() ) set ) )) = o : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) & f : ( ( V6() quasi_total bijective ) ( V6() quasi_total bijective ) Permutation of the carrier of b1 : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V11() V12() ) set ) ) . a : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V11() V12() ) set ) )) = b : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) ) ) ;

definition
let AFP be ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) ;
let f be ( ( V6() quasi_total bijective ) ( V6() quasi_total bijective ) Permutation of the carrier of AFP : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V11() V12() ) set ) ) ;
let K be ( ( ) ( ) Subset of ) ;
pred f is_Sc K means :: HOMOTHET:def 1
( f : ( ( ) ( ) M2(K19(K20(K20(AFP : ( ( ) ( ) AffinStruct ) ,AFP : ( ( ) ( ) AffinStruct ) ) : ( ( ) ( ) set ) ,K20(AFP : ( ( ) ( ) AffinStruct ) ,AFP : ( ( ) ( ) AffinStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) is collineation & K : ( ( ) ( ) M2(AFP : ( ( ) ( ) AffinStruct ) )) is being_line & ( for x being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st x : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) in K : ( ( ) ( ) M2(AFP : ( ( ) ( ) AffinStruct ) )) holds
f : ( ( ) ( ) M2(K19(K20(K20(AFP : ( ( ) ( ) AffinStruct ) ,AFP : ( ( ) ( ) AffinStruct ) ) : ( ( ) ( ) set ) ,K20(AFP : ( ( ) ( ) AffinStruct ) ,AFP : ( ( ) ( ) AffinStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) . x : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) : ( ( ) ( ) M2( the carrier of AFP : ( ( ) ( ) AffinStruct ) : ( ( ) ( ) set ) )) = x : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) ) & ( for x being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds x : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) ,f : ( ( ) ( ) M2(K19(K20(K20(AFP : ( ( ) ( ) AffinStruct ) ,AFP : ( ( ) ( ) AffinStruct ) ) : ( ( ) ( ) set ) ,K20(AFP : ( ( ) ( ) AffinStruct ) ,AFP : ( ( ) ( ) AffinStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) . x : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) : ( ( ) ( ) M2( the carrier of AFP : ( ( ) ( ) AffinStruct ) : ( ( ) ( ) set ) )) // K : ( ( ) ( ) M2(AFP : ( ( ) ( ) AffinStruct ) )) ) );
end;

theorem :: HOMOTHET:5
for AFP being ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane)
for p being ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) )
for K being ( ( ) ( ) Subset of )
for f being ( ( V6() quasi_total bijective ) ( V6() quasi_total bijective ) Permutation of the carrier of AFP : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V11() V12() ) set ) ) st f : ( ( V6() quasi_total bijective ) ( V6() quasi_total bijective ) Permutation of the carrier of b1 : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V11() V12() ) set ) ) is_Sc K : ( ( ) ( ) Subset of ) & f : ( ( V6() quasi_total bijective ) ( V6() quasi_total bijective ) Permutation of the carrier of b1 : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V11() V12() ) set ) ) . p : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V11() V12() ) set ) )) = p : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) & not p : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) in K : ( ( ) ( ) Subset of ) holds
f : ( ( V6() quasi_total bijective ) ( V6() quasi_total bijective ) Permutation of the carrier of b1 : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V11() V12() ) set ) ) = id the carrier of AFP : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V11() V12() ) set ) : ( ( V14( the carrier of b1 : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V11() V12() ) set ) ) ) ( V14( the carrier of b1 : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V11() V12() ) set ) ) ) M2(K19(K20( the carrier of b1 : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V11() V12() ) set ) , the carrier of b1 : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V11() V12() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ;

theorem :: HOMOTHET:6
for AFP being ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) st ( for a, b being ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) )
for K being ( ( ) ( ) Subset of ) st a : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) // K : ( ( ) ( ) Subset of ) & not a : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) in K : ( ( ) ( ) Subset of ) holds
ex f being ( ( V6() quasi_total bijective ) ( V6() quasi_total bijective ) Permutation of the carrier of AFP : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V11() V12() ) set ) ) st
( f : ( ( V6() quasi_total bijective ) ( V6() quasi_total bijective ) Permutation of the carrier of b1 : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V11() V12() ) set ) ) is_Sc K : ( ( ) ( ) Subset of ) & f : ( ( V6() quasi_total bijective ) ( V6() quasi_total bijective ) Permutation of the carrier of b1 : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V11() V12() ) set ) ) . a : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V11() V12() ) set ) )) = b : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) ) ) holds
AFP : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) is Moufangian ;

theorem :: HOMOTHET:7
for AFP being ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane)
for p, q, p9, q9, a, b, x, y being ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) )
for K, M being ( ( ) ( ) Subset of ) st K : ( ( ) ( ) Subset of ) // M : ( ( ) ( ) Subset of ) & p : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) in K : ( ( ) ( ) Subset of ) & q : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) in K : ( ( ) ( ) Subset of ) & p9 : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) in K : ( ( ) ( ) Subset of ) & q9 : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) in K : ( ( ) ( ) Subset of ) & AFP : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) is Moufangian & a : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) in M : ( ( ) ( ) Subset of ) & b : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) in M : ( ( ) ( ) Subset of ) & x : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) in M : ( ( ) ( ) Subset of ) & y : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) in M : ( ( ) ( ) Subset of ) & a : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) <> b : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) & q : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) <> p : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) & p : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) // p9 : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) & p : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) // p9 : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) & q : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) // q9 : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) holds
q : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) // q9 : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) ;

theorem :: HOMOTHET:8
for AFP being ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane)
for a, b being ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) )
for K being ( ( ) ( ) Subset of ) st a : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) // K : ( ( ) ( ) Subset of ) & not a : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) in K : ( ( ) ( ) Subset of ) & AFP : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) is Moufangian holds
ex f being ( ( V6() quasi_total bijective ) ( V6() quasi_total bijective ) Permutation of the carrier of AFP : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V11() V12() ) set ) ) st
( f : ( ( V6() quasi_total bijective ) ( V6() quasi_total bijective ) Permutation of the carrier of b1 : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V11() V12() ) set ) ) is_Sc K : ( ( ) ( ) Subset of ) & f : ( ( V6() quasi_total bijective ) ( V6() quasi_total bijective ) Permutation of the carrier of b1 : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V11() V12() ) set ) ) . a : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V11() V12() ) set ) )) = b : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) ) ;

theorem :: HOMOTHET:9
for AFP being ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) holds
( AFP : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) is Moufangian iff for a, b being ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) )
for K being ( ( ) ( ) Subset of ) st a : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) // K : ( ( ) ( ) Subset of ) & not a : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) in K : ( ( ) ( ) Subset of ) holds
ex f being ( ( V6() quasi_total bijective ) ( V6() quasi_total bijective ) Permutation of the carrier of AFP : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V11() V12() ) set ) ) st
( f : ( ( V6() quasi_total bijective ) ( V6() quasi_total bijective ) Permutation of the carrier of b1 : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V11() V12() ) set ) ) is_Sc K : ( ( ) ( ) Subset of ) & f : ( ( V6() quasi_total bijective ) ( V6() quasi_total bijective ) Permutation of the carrier of b1 : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V11() V12() ) set ) ) . a : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V11() V12() ) set ) )) = b : ( ( ) ( ) Element of ( ( ) ( V11() V12() ) set ) ) ) ) ;