:: PROJDES1 semantic presentation

theorem Th1: :: PROJDES1:1

for b₁ being up-3-dimensional 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 Th2: :: PROJDES1:2

canceled;

theorem Th3: :: PROJDES1:3

canceled;

theorem Th4: :: PROJDES1:4

canceled;

theorem Th5: :: PROJDES1:5

for b₁ being up-3-dimensional 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 Th6: :: PROJDES1:6

for b₁ being up-3-dimensional 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 Th7: :: PROJDES1:7

for b₁ being up-3-dimensional 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 Th8: :: PROJDES1:8

for b₁ being up-3-dimensional 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;

Lemma3: for b₁ being up-3-dimensional 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₅ holds
b₅ <> b₆

proof end;

definition

let c₁ be up-3-dimensional CollProjectiveSpace;
let c₂, c₃, c₄, c₅ be Element of c₁;
pred c₂,c₃,c₄,c₅ are_coplanar means :Def1: :: PROJDES1:def 1
ex b₁ being Element of a₁ st
( a₂,a₃,b₁ is_collinear & a₄,a₅,b₁ is_collinear );

end;

:: deftheorem Def1 defines are_coplanar PROJDES1:def 1 :

theorem Th9: :: PROJDES1:9

canceled;

theorem Th10: :: PROJDES1:10

for b₁ being up-3-dimensional CollProjectiveSpace
for b₂, b₃, b₄, b₅ being Element of b₁ st ( b₂,b₃,b₄ is_collinear or b₃,b₄,b₅ is_collinear or b₄,b₅,b₂ is_collinear or b₅,b₂,b₃ is_collinear ) holds
b₂,b₃,b₄,b₅ are_coplanar

proof end;

Lemma6: for b₁ being up-3-dimensional CollProjectiveSpace
for b₂, b₃, b₄, b₅ being Element of b₁ st b₂,b₃,b₄,b₅ are_coplanar holds
b₃,b₂,b₄,b₅ are_coplanar

proof end;

Lemma7: for b₁ being up-3-dimensional CollProjectiveSpace
for b₂, b₃, b₄, b₅ being Element of b₁ st b₂,b₃,b₄,b₅ are_coplanar holds
b₃,b₄,b₅,b₂ are_coplanar

proof end;

theorem Th11: :: PROJDES1:11

for b₁ being up-3-dimensional CollProjectiveSpace
for b₂, b₃, b₄, b₅ being Element of b₁ st b₂,b₃,b₄,b₅ are_coplanar holds
( b₃,b₄,b₅,b₂ are_coplanar & b₄,b₅,b₂,b₃ are_coplanar & b₅,b₂,b₃,b₄ are_coplanar & b₃,b₂,b₄,b₅ are_coplanar & b₄,b₃,b₅,b₂ are_coplanar & b₅,b₄,b₂,b₃ are_coplanar & b₂,b₅,b₃,b₄ are_coplanar & b₂,b₄,b₅,b₃ are_coplanar & b₃,b₅,b₂,b₄ are_coplanar & b₄,b₂,b₃,b₅ are_coplanar & b₅,b₃,b₄,b₂ are_coplanar & b₄,b₂,b₅,b₃ are_coplanar & b₅,b₃,b₂,b₄ are_coplanar & b₂,b₄,b₃,b₅ are_coplanar & b₃,b₅,b₄,b₂ are_coplanar & b₂,b₃,b₅,b₄ are_coplanar & b₂,b₅,b₄,b₃ are_coplanar & b₃,b₄,b₂,b₅ are_coplanar & b₃,b₂,b₅,b₄ are_coplanar & b₄,b₃,b₂,b₅ are_coplanar & b₄,b₅,b₃,b₂ are_coplanar & b₅,b₂,b₄,b₃ are_coplanar & b₅,b₄,b₃,b₂ are_coplanar )

proof end;

Lemma9: for b₁ being up-3-dimensional CollProjectiveSpace
for b₂, b₃, b₄, b₅, b₆ being Element of b₁ st not b₂,b₃,b₄ is_collinear & b₂,b₃,b₄,b₅ are_coplanar & b₂,b₃,b₄,b₆ are_coplanar holds
b₂,b₃,b₅,b₆ are_coplanar

proof end;

theorem Th12: :: PROJDES1:12

for b₁ being up-3-dimensional CollProjectiveSpace
for b₂, b₃, b₄, b₅, b₆, b₇, b₈ being Element of b₁ st not b₂,b₃,b₄ is_collinear & b₂,b₃,b₄,b₅ are_coplanar & b₂,b₃,b₄,b₆ are_coplanar & b₂,b₃,b₄,b₇ are_coplanar & b₂,b₃,b₄,b₈ are_coplanar holds
b₅,b₆,b₇,b₈ are_coplanar

proof end;

Lemma11: for b₁ being up-3-dimensional CollProjectiveSpace
for b₂, b₃, b₄, b₅, b₆, b₇ being Element of b₁ st not b₂,b₃,b₄ is_collinear & b₂,b₃,b₄,b₅ are_coplanar & b₂,b₃,b₄,b₆ are_coplanar & b₂,b₃,b₄,b₇ are_coplanar holds
b₂,b₅,b₆,b₇ are_coplanar

proof end;

theorem Th13: :: PROJDES1:13

for b₁ being up-3-dimensional CollProjectiveSpace
for b₂, b₃, b₄, b₅, b₆, b₇, b₈ being Element of b₁ st not b₂,b₃,b₄ is_collinear & b₅,b₆,b₇,b₂ are_coplanar & b₅,b₆,b₇,b₄ are_coplanar & b₅,b₆,b₇,b₃ are_coplanar & b₂,b₃,b₄,b₈ are_coplanar holds
b₅,b₆,b₇,b₈ are_coplanar

proof end;

Lemma12: for b₁ being up-3-dimensional CollProjectiveSpace
for b₂, b₃, b₄, b₅, b₆ being Element of b₁ st b₂ <> b₃ & b₂,b₃,b₄ is_collinear & b₅,b₆,b₂,b₃ are_coplanar holds
b₅,b₆,b₂,b₄ are_coplanar

proof end;

theorem Th14: :: PROJDES1:14

for b₁ being up-3-dimensional CollProjectiveSpace
for b₂, b₃, b₄, b₅, b₆, b₇ being Element of b₁ st b₂ <> b₃ & b₂,b₃,b₄ is_collinear & b₅,b₆,b₇,b₂ are_coplanar & b₅,b₆,b₇,b₃ are_coplanar holds
b₅,b₆,b₇,b₄ are_coplanar

proof end;

theorem Th15: :: PROJDES1:15

proof end;

theorem Th16: :: PROJDES1:16

for b₁ being up-3-dimensional CollProjectiveSpace holds
not for b₂, b₃, b₄, b₅ being Element of b₁ holds b₂,b₃,b₄,b₅ are_coplanar

proof end;

theorem Th17: :: PROJDES1:17

for b₁ being up-3-dimensional CollProjectiveSpace
for b₂, b₃, b₄ being Element of b₁ st not b₂,b₃,b₄ is_collinear holds
ex b₅ being Element of b₁ st not b₂,b₃,b₄,b₅ are_coplanar

proof end;

theorem Th18: :: PROJDES1:18

for b₁ being up-3-dimensional CollProjectiveSpace
for b₂, b₃, b₄, b₅ being Element of b₁ st ( b₂ = b₃ or b₂ = b₄ or b₃ = b₄ or b₂ = b₅ or b₃ = b₅ or b₅ = b₄ ) holds
b₂,b₃,b₄,b₅ are_coplanar

proof end;

theorem Th19: :: PROJDES1:19

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

proof end;

theorem Th20: :: PROJDES1:20

for b₁ being up-3-dimensional CollProjectiveSpace
for b₂, b₃, b₄, b₅, b₆, b₇, b₈, b₉, b₁₀ being Element of b₁ st not b₂,b₃,b₄ is_collinear & not b₅,b₆,b₇ is_collinear & b₂,b₃,b₄,b₈ are_coplanar & b₂,b₃,b₄,b₉ are_coplanar & b₂,b₃,b₄,b₁₀ are_coplanar & b₅,b₆,b₇,b₈ are_coplanar & b₅,b₆,b₇,b₉ are_coplanar & b₅,b₆,b₇,b₁₀ are_coplanar & not b₂,b₃,b₄,b₅ are_coplanar holds
b₈,b₉,b₁₀ is_collinear

proof end;

theorem Th21: :: PROJDES1:21

for b₁ being up-3-dimensional CollProjectiveSpace
for b₂, b₃, b₄, b₅, b₆, b₇, b₈, b₉, b₁₀, b₁₁ being Element of b₁ st b₂ <> b₃ & b₄,b₂,b₃ is_collinear & not b₂,b₅,b₆,b₄ are_coplanar & 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 holds
b₉,b₁₀,b₁₁ is_collinear

proof end;

theorem Th22: :: PROJDES1:22

for b₁ being up-3-dimensional CollProjectiveSpace
for b₂, b₃, b₄, b₅, b₆ being Element of b₁ st not b₂,b₃,b₄,b₅ are_coplanar & b₂,b₃,b₄,b₆ are_coplanar & not b₂,b₃,b₆ is_collinear holds
not b₂,b₃,b₅,b₆ are_coplanar

proof end;

theorem Th23: :: PROJDES1:23

for b₁ being up-3-dimensional CollProjectiveSpace
for b₂, b₃, b₄, b₅, b₆, b₇, b₈ being Element of b₁ st not b₂,b₃,b₄,b₅ are_coplanar & b₅,b₂,b₆ is_collinear & b₅,b₃,b₇ is_collinear & b₅,b₄,b₈ is_collinear & b₅ <> b₆ & b₅ <> b₇ & b₅ <> b₈ holds
( not b₆,b₇,b₈ is_collinear & not b₆,b₇,b₈,b₅ are_coplanar )

proof end;

theorem Th24: :: PROJDES1:24

for b₁ being up-3-dimensional CollProjectiveSpace
for b₂, b₃, b₄, b₅, b₆, b₇, b₈, b₉, b₁₀, b₁₁, b₁₂, b₁₃ being Element of b₁ st b₂,b₃,b₄,b₅ are_coplanar & not b₂,b₃,b₄,b₆ are_coplanar & not b₂,b₃,b₆,b₅ are_coplanar & not b₃,b₄,b₆,b₅ are_coplanar & not b₂,b₄,b₆,b₅ are_coplanar & 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₅ <> b₇ & b₆ <> b₇ & b₅ <> b₉ holds
not b₁₁,b₁₂,b₁₃ is_collinear

proof end;

definition

let c₁ be up-3-dimensional CollProjectiveSpace;
let c₂, c₃, c₄, c₅ be Element of c₁;
pred c₂,c₃,c₄,c₅ constitute_a_quadrangle means :Def2: :: PROJDES1:def 2
( not a₃,a₄,a₅ is_collinear & not a₂,a₃,a₄ is_collinear & not a₂,a₄,a₅ is_collinear & not a₂,a₅,a₃ is_collinear );

end;

:: deftheorem Def2 defines constitute_a_quadrangle PROJDES1:def 2 :

Lemma24: for b₁ being up-3-dimensional CollProjectiveSpace
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₆,b₇,b₈ constitute_a_quadrangle & 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 Th25: :: PROJDES1:25

canceled;

theorem Th26: :: PROJDES1:26

for b₁ being up-3-dimensional CollProjectiveSpace
for b₂, b₃, b₄, b₅, b₆, b₇, b₈, b₉, b₁₀, b₁₁ being Element of b₁ st 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₄,b₅,b₁₀ is_collinear & b₇,b₈,b₁₀ is_collinear & b₃,b₅,b₁₁ is_collinear & b₄ <> b₇ & b₆,b₈,b₁₁ is_collinear & b₂ <> b₆ & b₂ <> b₇ & b₂ <> b₈ holds
b₁₀,b₁₁,b₉ is_collinear

proof end;

theorem Th27: :: PROJDES1:27

for b₁ being up-3-dimensional CollProjectiveSpace holds b₁ is Desarguesian

proof end;

registration

cluster up-3-dimensional -> Desarguesian up-3-dimensional L5();
correctness by Th27;

end;