begin
theorem
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 ) ) ;
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
(
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
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 ) ) ;