:: HESSENBE semantic presentation

theorem Th1: :: HESSENBE:1

canceled;

theorem Th2: :: HESSENBE:2

canceled;

theorem Th3: :: HESSENBE:3

for b₁ being CollProjectiveSpace
for b₂, b₃, b₄ being Element of b₁ st b₂,b₃,b₄ is_collinear holds
( b₃,b₄,b₂ is_collinear & b₄,b₂,b₃ is_collinear & b₃,b₂,b₄ is_collinear & b₂,b₄,b₃ is_collinear & b₄,b₃,b₂ is_collinear )

proof end;

theorem Th4: :: HESSENBE:4

for b₁ being CollProjectiveSpace
for b₂, b₃, b₄, b₅ being Element of b₁ st b₂ <> b₃ & b₂,b₃,b₄ is_collinear & b₂,b₃,b₅ is_collinear holds
b₂,b₄,b₅ is_collinear

proof end;

theorem Th5: :: HESSENBE:5

for b₁ being CollProjectiveSpace
for b₂, b₃, b₄, b₅, b₆ being Element of b₁ st b₂ <> b₃ & b₄,b₅,b₂ is_collinear & b₄,b₅,b₃ is_collinear & b₂,b₃,b₆ is_collinear holds
b₄,b₅,b₆ is_collinear

proof end;

theorem Th6: :: HESSENBE:6

for b₁ being CollProjectiveSpace
for b₂, b₃ being Element of b₁ st b₂ <> b₃ holds
ex b₄ being Element of b₁ st not b₂,b₃,b₄ is_collinear

proof end;

theorem Th7: :: HESSENBE:7

for b₁ being CollProjectiveSpace
for b₂ being Element of b₁ holds
not for b₃, b₄ being Element of b₁ holds b₂,b₃,b₄ is_collinear

proof end;

theorem Th8: :: HESSENBE:8

for b₁ being CollProjectiveSpace
for b₂, b₃, b₄, b₅ being Element of b₁ st not b₂,b₃,b₄ is_collinear & b₂,b₃,b₅ is_collinear & b₂ <> b₅ holds
not b₂,b₅,b₄ is_collinear

proof end;

theorem Th9: :: HESSENBE:9

for b₁ being CollProjectiveSpace
for b₂, b₃, b₄, b₅ being Element of b₁ st not b₂,b₃,b₄ is_collinear & b₂,b₃,b₅ is_collinear & b₂,b₄,b₅ is_collinear holds
b₂ = b₅

proof end;

theorem Th10: :: HESSENBE:10

for b₁ being CollProjectiveSpace
for b₂, b₃, b₄, b₅, b₆, b₇ being Element of b₁ st not b₂,b₃,b₄ is_collinear & b₂,b₄,b₅ is_collinear & b₃,b₄,b₆ is_collinear & b₄ <> b₅ & b₇,b₅,b₆ is_collinear & b₂,b₃,b₇ is_collinear & b₂ <> b₇ holds
b₆ <> b₄

proof end;

theorem Th11: :: HESSENBE:11

canceled;

theorem Th12: :: HESSENBE:12

for b₁ being CollProjectiveSpace
for b₂, b₃, b₄, b₅, b₆, b₇ being Element of b₁ st not b₂,b₃,b₄ is_collinear & b₂,b₃,b₅ is_collinear & b₃,b₄,b₆ is_collinear & b₂,b₄,b₇ is_collinear & b₆,b₅,b₇ is_collinear & b₅ <> b₂ & b₅ <> b₃ & b₆ <> b₃ & b₆ <> b₄ holds
( b₂ <> b₇ & b₄ <> b₇ )

proof end;

theorem Th13: :: HESSENBE:13

for b₁ being CollProjectiveSpace
for b₂, b₃, b₄, b₅, b₆ being Element of b₁ st not b₂,b₃,b₄ is_collinear & b₂,b₃,b₅ is_collinear & b₄,b₆,b₅ is_collinear & b₆ <> b₄ & b₅ <> b₂ holds
not b₆,b₂,b₄ is_collinear

proof end;

theorem Th14: :: HESSENBE:14

for b₁ being CollProjectiveSpace
for b₂, b₃, b₄, b₅, b₆ being Element of b₁ st not b₂,b₃,b₄ is_collinear & b₂,b₃,b₅ is_collinear & b₄,b₅,b₆ is_collinear & b₂ <> b₅ & b₅ <> b₆ holds
not b₃,b₂,b₆ is_collinear

proof end;

theorem Th15: :: HESSENBE:15

for b₁ being CollProjectiveSpace
for b₂, b₃, b₄, b₅, b₆ being Element of b₁ st not b₂,b₃,b₄ is_collinear & b₂,b₃,b₅ is_collinear & b₄,b₆,b₅ is_collinear & b₅ <> b₆ & b₃ <> b₅ holds
not b₅,b₃,b₆ is_collinear

proof end;

theorem Th16: :: HESSENBE:16

for b₁ being CollProjectiveSpace
for b₂, b₃, b₄, b₅, b₆ being Element of b₁ st not b₂,b₃,b₄ is_collinear & b₂,b₃,b₅ is_collinear & b₄,b₆,b₂ is_collinear & b₂ <> b₅ & b₂ <> b₆ holds
not b₅,b₂,b₆ is_collinear

proof end;

theorem Th17: :: HESSENBE:17

for b₁ being CollProjectiveSpace
for b₂, b₃, b₄, b₅, b₆, b₇ being Element of b₁ st b₂ <> b₃ & b₄ <> b₅ & b₄,b₅,b₆ is_collinear & b₄,b₅,b₇ is_collinear & b₂,b₃,b₆ is_collinear & b₂,b₃,b₇ is_collinear & not b₂,b₃,b₄ is_collinear holds
b₆ = b₇

proof end;

theorem Th18: :: HESSENBE:18

canceled;

theorem Th19: :: HESSENBE:19

for b₁ being CollProjectiveSpace
for b₂, b₃, b₄, b₅, b₆ being Element of b₁ st not b₂,b₃,b₄ is_collinear & b₂,b₃,b₅ is_collinear & b₂,b₄,b₆ is_collinear & b₂ <> b₅ & b₂ <> b₆ holds
not b₂,b₅,b₆ is_collinear

proof end;

theorem Th20: :: HESSENBE:20

for b₁ being Pappian CollProjectivePlane
for b₂, b₃, b₄, b₅, b₆, b₇, b₈, b₉, b₁₀ being Element of b₁ st b₂ <> b₃ & b₄ <> b₃ & b₅ <> b₆ & b₇ <> b₅ & b₇ <> b₆ & not b₄,b₂,b₇ is_collinear & b₄,b₂,b₃ is_collinear & b₇,b₅,b₆ is_collinear & b₄,b₅,b₈ is_collinear & b₇,b₂,b₈ is_collinear & b₄,b₆,b₉ is_collinear & b₃,b₇,b₉ is_collinear & b₂,b₆,b₁₀ is_collinear & b₃,b₅,b₁₀ is_collinear holds
b₁₀,b₉,b₈ is_collinear

proof end;

Lemma14: for b₁ being Pappian CollProjectivePlane
for b₂, b₃, b₄, b₅, b₆, b₇, b₈, b₉, b₁₀, b₁₁ being Element of b₁ st b₂ <> b₃ & b₄ <> b₃ & b₂ <> b₅ & b₆ <> b₅ & b₂ <> b₇ & b₈ <> b₇ & not b₂,b₄,b₆ is_collinear & not b₂,b₄,b₈ is_collinear & not b₂,b₆,b₈ is_collinear & not b₂,b₉,b₁₀ is_collinear & b₄,b₆,b₁₀ is_collinear & b₃,b₅,b₁₀ is_collinear & b₆,b₈,b₉ is_collinear & b₅,b₇,b₉ is_collinear & b₄,b₈,b₁₁ is_collinear & b₃,b₇,b₁₁ is_collinear & b₂,b₄,b₃ is_collinear & b₂,b₆,b₅ is_collinear & b₂,b₈,b₇ is_collinear & ( b₄,b₆,b₈ is_collinear or b₃,b₅,b₇ is_collinear ) holds
b₉,b₁₁,b₁₀ is_collinear

proof end;

Lemma15: for b₁ being Pappian CollProjectivePlane
for b₂, b₃, b₄, b₅, b₆, b₇, b₈, b₉, b₁₀, b₁₁, b₁₂ being Element of b₁ st b₂ <> b₃ & b₄ <> b₃ & b₂ <> b₅ & b₆ <> b₅ & b₂ <> b₇ & b₈ <> b₇ & not b₂,b₄,b₆ is_collinear & not b₂,b₄,b₈ is_collinear & not b₂,b₆,b₈ is_collinear & not b₂,b₉,b₁₀ is_collinear & b₄,b₆,b₁₀ is_collinear & b₃,b₅,b₁₀ is_collinear & b₆,b₈,b₉ is_collinear & b₅,b₇,b₉ is_collinear & b₄,b₈,b₁₁ is_collinear & b₃,b₇,b₁₁ is_collinear & b₂,b₄,b₃ is_collinear & b₂,b₆,b₅ is_collinear & b₂,b₈,b₇ is_collinear & b₂,b₆,b₁₂ is_collinear & b₄,b₈,b₁₂ is_collinear & not b₉,b₁₀,b₁₂ is_collinear holds
b₉,b₁₁,b₁₀ is_collinear

proof end;

Lemma16: for b₁ being Pappian CollProjectivePlane
for b₂, b₃, b₄, b₅, b₆, b₇, b₈, b₉, b₁₀, b₁₁ being Element of b₁ st b₂ <> b₃ & b₄ <> b₃ & b₂ <> b₅ & b₆ <> b₅ & b₂ <> b₇ & b₈ <> b₇ & not b₂,b₄,b₆ is_collinear & not b₂,b₄,b₈ is_collinear & not b₂,b₆,b₈ is_collinear & not b₂,b₉,b₁₀ is_collinear & b₄,b₆,b₁₀ is_collinear & b₃,b₅,b₁₀ is_collinear & b₆,b₈,b₉ is_collinear & b₅,b₇,b₉ is_collinear & b₄,b₈,b₁₁ is_collinear & b₃,b₇,b₁₁ is_collinear & b₂,b₄,b₃ is_collinear & b₂,b₆,b₅ is_collinear & b₂,b₈,b₇ is_collinear holds
b₉,b₁₁,b₁₀ is_collinear

proof end;

theorem Th21: :: HESSENBE:21

for b₁ being Pappian CollProjectivePlane
for b₂, b₃, b₄, b₅, b₆, b₇, b₈, b₉, b₁₀, b₁₁ being Element of b₁ st b₂ <> b₃ & b₄ <> b₃ & b₂ <> b₅ & b₆ <> b₅ & b₂ <> b₇ & b₈ <> b₇ & not b₂,b₄,b₆ is_collinear & not b₂,b₄,b₈ is_collinear & not b₂,b₆,b₈ is_collinear & b₄,b₆,b₉ is_collinear & b₃,b₅,b₉ is_collinear & b₆,b₈,b₁₀ is_collinear & b₅,b₇,b₁₀ is_collinear & b₄,b₈,b₁₁ is_collinear & b₃,b₇,b₁₁ is_collinear & b₂,b₄,b₃ is_collinear & b₂,b₆,b₅ is_collinear & b₂,b₈,b₇ is_collinear holds
b₁₀,b₁₁,b₉ is_collinear

proof end;

registration

cluster Pappian -> Desarguesian L5();
coherence

proof end;

end;