begin
theorem
for
SAS being ( (
V46()
AffinSpace-like 2-dimensional ) (
V41()
V46()
AffinSpace-like 2-dimensional )
AffinPlane) st
SAS : ( (
V46()
AffinSpace-like 2-dimensional ) (
V41()
V46()
AffinSpace-like 2-dimensional )
AffinPlane) is
Pappian holds
for
a1,
a2,
a3,
b1,
b2,
b3 being ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) st
a1 : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ,
a2 : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) )
// a1 : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ,
a3 : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) &
b1 : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ,
b2 : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) )
// b1 : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ,
b3 : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) &
a1 : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ,
b2 : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) )
// a2 : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ,
b1 : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) &
a2 : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ,
b3 : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) )
// a3 : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ,
b2 : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) holds
a3 : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ,
b1 : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) )
// a1 : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ,
b3 : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ;
theorem
for
SAS being ( (
V46()
AffinSpace-like 2-dimensional ) (
V41()
V46()
AffinSpace-like 2-dimensional )
AffinPlane) st
SAS : ( (
V46()
AffinSpace-like 2-dimensional ) (
V41()
V46()
AffinSpace-like 2-dimensional )
AffinPlane) is
Desarguesian holds
for
o,
a,
a9,
b,
b9,
c,
c9 being ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) st not
o : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ,
a : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) )
// o : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ,
b : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) & not
o : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ,
a : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) )
// o : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ,
c : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) &
o : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ,
a : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) )
// o : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ,
a9 : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) &
o : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ,
b : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) )
// o : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ,
b9 : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) &
o : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ,
c : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) )
// o : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ,
c9 : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) &
a : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ,
b : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) )
// a9 : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ,
b9 : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) &
a : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ,
c : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) )
// a9 : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ,
c9 : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) holds
b : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ,
c : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) )
// b9 : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ,
c9 : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ;
theorem
for
SAS being ( (
V46()
AffinSpace-like 2-dimensional ) (
V41()
V46()
AffinSpace-like 2-dimensional )
AffinPlane) st
SAS : ( (
V46()
AffinSpace-like 2-dimensional ) (
V41()
V46()
AffinSpace-like 2-dimensional )
AffinPlane) is
translational holds
for
a,
a9,
b,
b9,
c,
c9 being ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) st not
a : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ,
a9 : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) )
// a : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ,
b : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) & not
a : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ,
a9 : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) )
// a : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ,
c : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) &
a : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ,
a9 : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) )
// b : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ,
b9 : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) &
a : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ,
a9 : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) )
// c : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ,
c9 : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) &
a : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ,
b : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) )
// a9 : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ,
b9 : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) &
a : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ,
c : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) )
// a9 : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ,
c9 : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) holds
b : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ,
c : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) )
// b9 : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ,
c9 : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ;
theorem
ex
SAS being ( (
V46()
AffinSpace-like 2-dimensional ) (
V41()
V46()
AffinSpace-like 2-dimensional )
AffinPlane) st
( ( for
o,
a,
a9,
b,
b9,
c,
c9 being ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) st not
o : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ,
a : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) )
// o : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ,
b : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) & not
o : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ,
a : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) )
// o : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ,
c : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) &
o : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ,
a : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) )
// o : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ,
a9 : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) &
o : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ,
b : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) )
// o : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ,
b9 : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) &
o : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ,
c : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) )
// o : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ,
c9 : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) &
a : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ,
b : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) )
// a9 : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ,
b9 : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) &
a : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ,
c : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) )
// a9 : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ,
c9 : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) holds
b : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ,
c : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) )
// b9 : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ,
c9 : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ) & ( for
a,
a9,
b,
b9,
c,
c9 being ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) st not
a : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ,
a9 : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) )
// a : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ,
b : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) & not
a : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ,
a9 : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) )
// a : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ,
c : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) &
a : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ,
a9 : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) )
// b : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ,
b9 : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) &
a : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ,
a9 : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) )
// c : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ,
c9 : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) &
a : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ,
b : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) )
// a9 : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ,
b9 : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) &
a : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ,
c : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) )
// a9 : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ,
c9 : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) holds
b : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ,
c : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) )
// b9 : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ,
c9 : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ) & ( for
a1,
a2,
a3,
b1,
b2,
b3 being ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) st
a1 : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ,
a2 : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) )
// a1 : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ,
a3 : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) &
b1 : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ,
b2 : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) )
// b1 : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ,
b3 : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) &
a1 : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ,
b2 : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) )
// a2 : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ,
b1 : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) &
a2 : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ,
b3 : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) )
// a3 : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ,
b2 : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) holds
a3 : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ,
b1 : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) )
// a1 : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ,
b3 : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ) & ( for
a,
b,
c,
d being ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) st not
a : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ,
b : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) )
// a : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ,
c : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) &
a : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ,
b : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) )
// c : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ,
d : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) &
a : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ,
c : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) )
// b : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ,
d : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) holds
not
a : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ,
d : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) )
// b : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ,
c : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ) ) ;
theorem
for
SAS being ( (
V46()
AffinSpace-like 2-dimensional ) (
V41()
V46()
AffinSpace-like 2-dimensional )
AffinPlane)
for
o,
a being ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ex
p being ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) st
for
b,
c being ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) holds
(
o : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ,
a : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) )
// o : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ,
p : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) & ex
d being ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) st
(
o : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ,
p : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) )
// o : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ,
b : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) implies (
o : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ,
c : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) )
// o : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ,
d : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) &
p : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ,
c : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) )
// b : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ,
d : ( ( ) ( )
Element of ( ( ) (
V4()
V5() )
set ) ) ) ) ) ;