:: HESSENBE semantic presentation

theorem :: HESSENBE:1

canceled;

theorem :: HESSENBE:2

canceled;

theorem Th3: :: HESSENBE:3

for PCPP being CollProjectiveSpace
for a, b, c being Element of PCPP st a,b,c is_collinear holds
( b,c,a is_collinear & c,a,b is_collinear & b,a,c is_collinear & a,c,b is_collinear & c,b,a is_collinear )

proof end;

theorem Th4: :: HESSENBE:4

for PCPP being CollProjectiveSpace
for a, b, c, d being Element of PCPP st a <> b & a,b,c is_collinear & a,b,d is_collinear holds
a,c,d is_collinear

proof end;

theorem :: HESSENBE:5

for PCPP being CollProjectiveSpace
for p, q, a, b, r being Element of PCPP st p <> q & a,b,p is_collinear & a,b,q is_collinear & p,q,r is_collinear holds
a,b,r is_collinear

proof end;

theorem Th6: :: HESSENBE:6

for PCPP being CollProjectiveSpace
for p, q being Element of PCPP st p <> q holds
ex r being Element of PCPP st not p,q,r is_collinear

proof end;

theorem :: HESSENBE:7

for PCPP being CollProjectiveSpace
for p being Element of PCPP holds
not for q, r being Element of PCPP holds p,q,r is_collinear

proof end;

theorem Th8: :: HESSENBE:8

for PCPP being CollProjectiveSpace
for a, b, c, b' being Element of PCPP st not a,b,c is_collinear & a,b,b' is_collinear & a <> b' holds
not a,b',c is_collinear

proof end;

theorem Th9: :: HESSENBE:9

for PCPP being CollProjectiveSpace
for a, b, c, d being Element of PCPP st not a,b,c is_collinear & a,b,d is_collinear & a,c,d is_collinear holds
a = d

proof end;

theorem Th10: :: HESSENBE:10

for PCPP being CollProjectiveSpace
for o, a, d, d', x, a' being Element of PCPP st not o,a,d is_collinear & o,d,d' is_collinear & a,d,x is_collinear & d <> d' & a',d',x is_collinear & o,a,a' is_collinear & o <> a' holds
x <> d

proof end;

theorem :: HESSENBE:11

canceled;

theorem Th12: :: HESSENBE:12

for PCPP being CollProjectiveSpace
for a1, a2, a3, c3, c1, x being Element of PCPP st not a1,a2,a3 is_collinear & a1,a2,c3 is_collinear & a2,a3,c1 is_collinear & a1,a3,x is_collinear & c1,c3,x is_collinear & c3 <> a1 & c3 <> a2 & c1 <> a2 & c1 <> a3 holds
( a1 <> x & a3 <> x )

proof end;

theorem Th13: :: HESSENBE:13

for PCPP being CollProjectiveSpace
for a, b, c, d, e being Element of PCPP st not a,b,c is_collinear & a,b,d is_collinear & c,e,d is_collinear & e <> c & d <> a holds
not e,a,c is_collinear

proof end;

theorem Th14: :: HESSENBE:14

for PCPP being CollProjectiveSpace
for p1, p2, q1, q2, q3 being Element of PCPP st not p1,p2,q1 is_collinear & p1,p2,q2 is_collinear & q1,q2,q3 is_collinear & p1 <> q2 & q2 <> q3 holds
not p2,p1,q3 is_collinear

proof end;

theorem :: HESSENBE:15

for PCPP being CollProjectiveSpace
for p1, p2, q1, p3, q2 being Element of PCPP st not p1,p2,q1 is_collinear & p1,p2,p3 is_collinear & q1,q2,p3 is_collinear & p3 <> q2 & p2 <> p3 holds
not p3,p2,q2 is_collinear

proof end;

theorem Th16: :: HESSENBE:16

for PCPP being CollProjectiveSpace
for p1, p2, q1, p3, q2 being Element of PCPP st not p1,p2,q1 is_collinear & p1,p2,p3 is_collinear & q1,q2,p1 is_collinear & p1 <> p3 & p1 <> q2 holds
not p3,p1,q2 is_collinear

proof end;

theorem Th17: :: HESSENBE:17

for PCPP being CollProjectiveSpace
for a1, a2, b1, b2, x, y being Element of PCPP st a1 <> a2 & b1 <> b2 & b1,b2,x is_collinear & b1,b2,y is_collinear & a1,a2,x is_collinear & a1,a2,y is_collinear & not a1,a2,b1 is_collinear holds
x = y

proof end;

theorem :: HESSENBE:18

canceled;

theorem Th19: :: HESSENBE:19

for PCPP being CollProjectiveSpace
for o, a1, a2, b1, b2 being Element of PCPP st not o,a1,a2 is_collinear & o,a1,b1 is_collinear & o,a2,b2 is_collinear & o <> b1 & o <> b2 holds
not o,b1,b2 is_collinear

proof end;

theorem Th20: :: HESSENBE:20

for PCPP being Pappian CollProjectivePlane
for p2, p3, p1, q2, q3, q1, r3, r2, r1 being Element of PCPP st p2 <> p3 & p1 <> p3 & q2 <> q3 & q1 <> q2 & q1 <> q3 & not p1,p2,q1 is_collinear & p1,p2,p3 is_collinear & q1,q2,q3 is_collinear & p1,q2,r3 is_collinear & q1,p2,r3 is_collinear & p1,q3,r2 is_collinear & p3,q1,r2 is_collinear & p2,q3,r1 is_collinear & p3,q2,r1 is_collinear holds
r1,r2,r3 is_collinear

proof end;

Lm1: for PCPP being Pappian CollProjectivePlane
for o, b1, a1, b2, a2, b3, a3, c1, c3, c2 being Element of PCPP st o <> b1 & a1 <> b1 & o <> b2 & a2 <> b2 & o <> b3 & a3 <> b3 & not o,a1,a2 is_collinear & not o,a1,a3 is_collinear & not o,a2,a3 is_collinear & not o,c1,c3 is_collinear & a1,a2,c3 is_collinear & b1,b2,c3 is_collinear & a2,a3,c1 is_collinear & b2,b3,c1 is_collinear & a1,a3,c2 is_collinear & b1,b3,c2 is_collinear & o,a1,b1 is_collinear & o,a2,b2 is_collinear & o,a3,b3 is_collinear & ( a1,a2,a3 is_collinear or b1,b2,b3 is_collinear ) holds
c1,c2,c3 is_collinear

proof end;

Lm2: for PCPP being Pappian CollProjectivePlane
for o, b1, a1, b2, a2, b3, a3, c1, c3, c2, x being Element of PCPP st o <> b1 & a1 <> b1 & o <> b2 & a2 <> b2 & o <> b3 & a3 <> b3 & not o,a1,a2 is_collinear & not o,a1,a3 is_collinear & not o,a2,a3 is_collinear & not o,c1,c3 is_collinear & a1,a2,c3 is_collinear & b1,b2,c3 is_collinear & a2,a3,c1 is_collinear & b2,b3,c1 is_collinear & a1,a3,c2 is_collinear & b1,b3,c2 is_collinear & o,a1,b1 is_collinear & o,a2,b2 is_collinear & o,a3,b3 is_collinear & o,a2,x is_collinear & a1,a3,x is_collinear & not c1,c3,x is_collinear holds
c1,c2,c3 is_collinear

proof end;

Lm3: for PCPP being Pappian CollProjectivePlane
for o, b1, a1, b2, a2, b3, a3, c1, c3, c2 being Element of PCPP st o <> b1 & a1 <> b1 & o <> b2 & a2 <> b2 & o <> b3 & a3 <> b3 & not o,a1,a2 is_collinear & not o,a1,a3 is_collinear & not o,a2,a3 is_collinear & not o,c1,c3 is_collinear & a1,a2,c3 is_collinear & b1,b2,c3 is_collinear & a2,a3,c1 is_collinear & b2,b3,c1 is_collinear & a1,a3,c2 is_collinear & b1,b3,c2 is_collinear & o,a1,b1 is_collinear & o,a2,b2 is_collinear & o,a3,b3 is_collinear holds
c1,c2,c3 is_collinear

proof end;

theorem Th21: :: HESSENBE:21

for PCPP being Pappian CollProjectivePlane
for o, b1, a1, b2, a2, b3, a3, c3, c1, c2 being Element of PCPP st o <> b1 & a1 <> b1 & o <> b2 & a2 <> b2 & o <> b3 & a3 <> b3 & not o,a1,a2 is_collinear & not o,a1,a3 is_collinear & not o,a2,a3 is_collinear & a1,a2,c3 is_collinear & b1,b2,c3 is_collinear & a2,a3,c1 is_collinear & b2,b3,c1 is_collinear & a1,a3,c2 is_collinear & b1,b3,c2 is_collinear & o,a1,b1 is_collinear & o,a2,b2 is_collinear & o,a3,b3 is_collinear holds
c1,c2,c3 is_collinear

proof end;

registration

cluster Pappian -> Desarguesian L5();
coherence

proof end;

end;