HESSENBE

theorem :: HESSENBE:1

for PCPP being ( ( V38() V101() V102() proper Vebleian at_least_3rank ) ( V38() V101() V102() proper Vebleian at_least_3rank ) CollProjectiveSpace)
for a, b, c being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear holds
( b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear ) ;

theorem :: HESSENBE:2

for PCPP being ( ( V38() V101() V102() proper Vebleian at_least_3rank ) ( V38() V101() V102() proper Vebleian at_least_3rank ) CollProjectiveSpace)
for a, b, c, d being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear holds
a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear ;

theorem :: HESSENBE:3

for PCPP being ( ( V38() V101() V102() proper Vebleian at_least_3rank ) ( V38() V101() V102() proper Vebleian at_least_3rank ) CollProjectiveSpace)
for p, q, a, b, r being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st p : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> q : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & p : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,r : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear holds
a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,r : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear ;

theorem :: HESSENBE:6

for PCPP being ( ( V38() V101() V102() proper Vebleian at_least_3rank ) ( V38() V101() V102() proper Vebleian at_least_3rank ) CollProjectiveSpace)
for a, b, c, b9 being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st not a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> b9 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds
not a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear ;

theorem :: HESSENBE:7

for PCPP being ( ( V38() V101() V102() proper Vebleian at_least_3rank ) ( V38() V101() V102() proper Vebleian at_least_3rank ) CollProjectiveSpace)
for a, b, c, d being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st not a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear holds
a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) = d : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ;

theorem :: HESSENBE:8

for PCPP being ( ( V38() V101() V102() proper Vebleian at_least_3rank ) ( V38() V101() V102() proper Vebleian at_least_3rank ) CollProjectiveSpace)
for o, a, d, d9, a9, x being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st not o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,d9 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & d : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> d9 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & a9 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,d9 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a9 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> a9 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds
x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> d : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ;

theorem :: HESSENBE:9

for PCPP being ( ( V38() V101() V102() proper Vebleian at_least_3rank ) ( V38() V101() V102() proper Vebleian at_least_3rank ) CollProjectiveSpace)
for a1, a2, a3, c3, c1, x being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st not a1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a2 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a3 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & a1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a2 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c3 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & a2 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a3 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & c1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c3 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & c3 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> a1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & c3 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> a2 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & c1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> a2 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & c1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> a3 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds
( a1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & a3 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) ;

theorem :: HESSENBE:10

for PCPP being ( ( V38() V101() V102() proper Vebleian at_least_3rank ) ( V38() V101() V102() proper Vebleian at_least_3rank ) CollProjectiveSpace)
for a, b, c, d, e being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st not a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,e : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & e : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & d : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds
not e : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear ;

theorem :: HESSENBE:11

for PCPP being ( ( V38() V101() V102() proper Vebleian at_least_3rank ) ( V38() V101() V102() proper Vebleian at_least_3rank ) CollProjectiveSpace)
for p1, p2, q1, q2, q3 being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st not p1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,p2 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,q1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & p1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,p2 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,q2 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & q1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,q2 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,q3 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & q2 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> q3 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds
not p2 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,p1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,q3 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear ;

theorem :: HESSENBE:12

for PCPP being ( ( V38() V101() V102() proper Vebleian at_least_3rank ) ( V38() V101() V102() proper Vebleian at_least_3rank ) CollProjectiveSpace)
for p1, p2, q1, p3, q2 being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st not p1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,p2 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,q1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & p1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,p2 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,p3 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & q1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,q2 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,p3 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & p3 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> q2 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & p2 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> p3 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds
not p3 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,p2 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,q2 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear ;

theorem :: HESSENBE:13

for PCPP being ( ( V38() V101() V102() proper Vebleian at_least_3rank ) ( V38() V101() V102() proper Vebleian at_least_3rank ) CollProjectiveSpace)
for p1, p2, q1, p3, q2 being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st not p1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,p2 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,q1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & p1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,p2 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,p3 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & q1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,q2 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,p1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & p1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> p3 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & p1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> q2 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds
not p3 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,p1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,q2 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear ;

theorem :: HESSENBE:14

for PCPP being ( ( V38() V101() V102() proper Vebleian at_least_3rank ) ( V38() V101() V102() proper Vebleian at_least_3rank ) CollProjectiveSpace)
for a1, a2, b1, b2, x, y being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st a1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> a2 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & b1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> b2 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & b1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b2 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & b1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b2 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & a1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a2 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & a1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a2 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & not a1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a2 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear holds
x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) = y : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ;

theorem :: HESSENBE:15

for PCPP being ( ( V38() V101() V102() proper Vebleian at_least_3rank ) ( V38() V101() V102() proper Vebleian at_least_3rank ) CollProjectiveSpace)
for o, a1, a2, b1, b2 being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st not o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a2 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a2 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b2 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> b1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> b2 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds
not o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b2 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear ;

theorem :: HESSENBE:16

for PCPP being ( ( V38() V101() V102() proper Vebleian at_least_3rank Pappian non up-3-dimensional ) ( V38() V101() V102() proper Vebleian at_least_3rank Pappian non up-3-dimensional ) CollProjectivePlane)
for p2, p3, p1, q2, q3, q1, r3, r2, r1 being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st p2 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> p3 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & p1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> p3 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & q2 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> q3 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & q1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> q2 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & q1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> q3 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & not p1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,p2 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,q1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & p1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,p2 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,p3 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & q1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,q2 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,q3 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & p1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,q2 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,r3 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & q1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,p2 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,r3 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & p1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,q3 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,r2 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & p3 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,q1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,r2 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & p2 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,q3 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,r1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & p3 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,q2 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,r1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear holds
r1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,r2 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,r3 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear ;

theorem :: HESSENBE:17

for PCPP being ( ( V38() V101() V102() proper Vebleian at_least_3rank Pappian non up-3-dimensional ) ( V38() V101() V102() proper Vebleian at_least_3rank Pappian non up-3-dimensional ) CollProjectivePlane)
for o, b1, a1, b2, a2, b3, a3, c3, c1, c2 being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> b1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & a1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> b1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> b2 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & a2 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> b2 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> b3 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & a3 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> b3 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & not o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a2 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & not o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a3 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & not o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a2 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a3 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & a1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a2 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c3 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & b1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b2 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c3 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & a2 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a3 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & b2 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b3 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & a1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a3 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c2 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & b1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b3 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c2 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a2 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b2 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a3 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b3 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear holds
c1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c2 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c3 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear ;