:: GEOMTRAP semantic presentation

definition

let c₁ be RealLinearSpace;
let c₂, c₃, c₄, c₅ be VECTOR of c₁;
pred c₂,c₃ '||' c₄,c₅ means :Def1: :: GEOMTRAP:def 1
( a₂,a₃ // a₄,a₅ or a₂,a₃ // a₅,a₄ );

end;

:: deftheorem Def1 defines '||' GEOMTRAP:def 1 :

theorem Th1: :: GEOMTRAP:1

for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁ st Gen b₂,b₃ holds
OASpace b₁ is OAffinSpace

proof end;

theorem Th2: :: GEOMTRAP:2

for b₁ being RealLinearSpace
for b₂, b₃, b₄, b₅ being VECTOR of b₁
for b₆, b₇, b₈, b₉ being Element of (OASpace b₁) st b₆ = b₂ & b₇ = b₃ & b₈ = b₄ & b₉ = b₅ holds
( b₆,b₇ // b₈,b₉ iff b₂,b₃ // b₄,b₅ )

proof end;

theorem Th3: :: GEOMTRAP:3

for b₁ being RealLinearSpace
for b₂, b₃, b₄, b₅, b₆, b₇ being VECTOR of b₁ st Gen b₂,b₃ holds
for b₈, b₉, b₁₀, b₁₁ being Element of the carrier of (Lambda (OASpace b₁)) st b₈ = b₄ & b₉ = b₅ & b₁₀ = b₆ & b₁₁ = b₇ holds
( b₈,b₉ // b₁₀,b₁₁ iff b₄,b₅ '||' b₆,b₇ )

proof end;

theorem Th4: :: GEOMTRAP:4

for b₁ being RealLinearSpace
for b₂, b₃, b₄, b₅, b₆, b₇ being VECTOR of b₁
for b₈, b₉, b₁₀, b₁₁ being Element of the carrier of (AMSpace b₁,b₂,b₃) st b₈ = b₄ & b₉ = b₅ & b₁₀ = b₆ & b₁₁ = b₇ holds
( b₈,b₉ // b₁₀,b₁₁ iff b₄,b₅ '||' b₆,b₇ )

proof end;

definition

let c₁ be RealLinearSpace;
let c₂, c₃ be VECTOR of c₁;
func c₂ # c₃ -> VECTOR of a₁ means :Def2: :: GEOMTRAP:def 2
a₄ + a₄ = a₂ + a₃;
existence

proof end;

uniqueness

proof end;

commutativity ;
idempotence ;

end;

:: deftheorem Def2 defines # GEOMTRAP:def 2 :

theorem Th5: :: GEOMTRAP:5

canceled;

theorem Th6: :: GEOMTRAP:6

canceled;

theorem Th7: :: GEOMTRAP:7

for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁ ex b₄ being VECTOR of b₁ st b₂ # b₄ = b₃

proof end;

theorem Th8: :: GEOMTRAP:8

for b₁ being RealLinearSpace
for b₂, b₃, b₄, b₅ being VECTOR of b₁ holds (b₂ # b₃) # (b₄ # b₅) = (b₂ # b₄) # (b₃ # b₅)

proof end;

theorem Th9: :: GEOMTRAP:9

for b₁ being RealLinearSpace
for b₂, b₃, b₄ being VECTOR of b₁ st b₂ # b₃ = b₂ # b₄ holds
b₃ = b₄

proof end;

theorem Th10: :: GEOMTRAP:10

for b₁ being RealLinearSpace
for b₂, b₃, b₄ being VECTOR of b₁ holds b₂,b₃ // b₄ # b₂,b₄ # b₃

proof end;

theorem Th11: :: GEOMTRAP:11

for b₁ being RealLinearSpace
for b₂, b₃, b₄ being VECTOR of b₁ holds b₂,b₃ '||' b₄ # b₂,b₄ # b₃

proof end;

theorem Th12: :: GEOMTRAP:12

for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁ holds
( 2 * ((b₂ # b₃) - b₂) = b₃ - b₂ & 2 * (b₃ - (b₂ # b₃)) = b₃ - b₂ )

proof end;

theorem Th13: :: GEOMTRAP:13

for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁ holds b₂,b₂ # b₃ // b₂ # b₃,b₃

proof end;

theorem Th14: :: GEOMTRAP:14

for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁ holds
( b₂,b₃ // b₂,b₂ # b₃ & b₂,b₃ // b₂ # b₃,b₃ )

proof end;

Lemma14: for b₁ being RealLinearSpace
for b₂, b₃, b₄ being VECTOR of b₁ st b₂,b₃ // b₃,b₄ holds
( b₄,b₃ // b₃,b₂ & b₂,b₃ // b₂,b₄ & b₃,b₄ // b₂,b₄ )

proof end;

theorem Th15: :: GEOMTRAP:15

for b₁ being RealLinearSpace
for b₂, b₃, b₄ being VECTOR of b₁ st b₂,b₃ // b₃,b₄ holds
b₂ # b₃,b₃ // b₃,b₃ # b₄

proof end;

theorem Th16: :: GEOMTRAP:16

for b₁ being RealLinearSpace
for b₂, b₃, b₄, b₅ being VECTOR of b₁ st b₂,b₃ // b₄,b₅ holds
b₂,b₃ // b₂ # b₄,b₃ # b₅

proof end;

Lemma17: for b₁ being RealLinearSpace
for b₂, b₃, b₄, b₅ being VECTOR of b₁ st b₂,b₃ // b₄,b₅ holds
b₂,b₃ '||' b₂ # b₅,b₃ # b₄

proof end;

Lemma18: for b₁ being RealLinearSpace
for b₂, b₃, b₄, b₅ being VECTOR of b₁ st b₂ # b₃ = b₄ # b₅ holds
b₄ - b₂ = - (b₅ - b₃)

proof end;

Lemma19: for b₁ being RealLinearSpace
for b₂, b₃, b₄, b₅, b₆, b₇ being VECTOR of b₁ st Gen b₂,b₃ & b₄,b₅,b₆,b₇ are_Ort_wrt b₂,b₃ holds
( b₆,b₇,b₄,b₅ are_Ort_wrt b₂,b₃ & b₄,b₅,b₇,b₆ are_Ort_wrt b₂,b₃ )

proof end;

Lemma20: for b₁ being RealLinearSpace
for b₂, b₃, b₄, b₅, b₆ being VECTOR of b₁ st Gen b₂,b₃ holds
b₄,b₅,b₆,b₆ are_Ort_wrt b₂,b₃

proof end;

Lemma21: for b₁ being RealLinearSpace
for b₂, b₃, b₄, b₅, b₆, b₇, b₈ being VECTOR of b₁ st Gen b₂,b₃ & b₄,b₅,b₆,b₇ are_Ort_wrt b₂,b₃ & b₄,b₅,b₆,b₈ are_Ort_wrt b₂,b₃ holds
b₄,b₅,b₇,b₈ are_Ort_wrt b₂,b₃

proof end;

Lemma22: for b₁ being RealLinearSpace
for b₂, b₃, b₄, b₅ being VECTOR of b₁ st Gen b₂,b₃ & b₄,b₅,b₄,b₅ are_Ort_wrt b₂,b₃ holds
b₄ = b₅

proof end;

Lemma23: for b₁ being RealLinearSpace
for b₂, b₃, b₄, b₅, b₆ being VECTOR of b₁ st Gen b₂,b₃ holds
( b₄,b₅,b₆,b₆ are_Ort_wrt b₂,b₃ & b₆,b₆,b₄,b₅ are_Ort_wrt b₂,b₃ )

proof end;

Lemma24: for b₁ being RealLinearSpace
for b₂, b₃, b₄, b₅, b₆, b₇, b₈, b₉ being VECTOR of b₁ st Gen b₂,b₃ & ( b₄,b₅ '||' b₆,b₇ or b₆,b₇ '||' b₄,b₅ ) & ( b₈,b₉,b₆,b₇ are_Ort_wrt b₂,b₃ or b₆,b₇,b₈,b₉ are_Ort_wrt b₂,b₃ ) & b₆ <> b₇ holds
( b₄,b₅,b₈,b₉ are_Ort_wrt b₂,b₃ & b₈,b₉,b₄,b₅ are_Ort_wrt b₂,b₃ )

proof end;

definition

let c₁ be RealLinearSpace;
let c₂, c₃, c₄, c₅, c₆, c₇ be VECTOR of c₁;
pred c₄,c₅,c₆,c₇ are_DTr_wrt c₂,c₃ means :Def3: :: GEOMTRAP:def 3
( a₄,a₅ // a₆,a₇ & a₄,a₅,a₄ # a₅,a₆ # a₇ are_Ort_wrt a₂,a₃ & a₆,a₇,a₄ # a₅,a₆ # a₇ are_Ort_wrt a₂,a₃ );

end;

:: deftheorem Def3 defines are_DTr_wrt GEOMTRAP:def 3 :

theorem Th17: :: GEOMTRAP:17

for b₁ being RealLinearSpace
for b₂, b₃, b₄, b₅ being VECTOR of b₁ st Gen b₂,b₃ holds
b₄,b₄,b₅,b₅ are_DTr_wrt b₂,b₃

proof end;

theorem Th18: :: GEOMTRAP:18

for b₁ being RealLinearSpace
for b₂, b₃, b₄, b₅ being VECTOR of b₁ st Gen b₂,b₃ holds
b₄,b₅,b₄,b₅ are_DTr_wrt b₂,b₃

proof end;

theorem Th19: :: GEOMTRAP:19

for b₁ being RealLinearSpace
for b₂, b₃, b₄, b₅ being VECTOR of b₁ st b₂,b₃,b₃,b₂ are_DTr_wrt b₄,b₅ holds
b₂ = b₃

proof end;

theorem Th20: :: GEOMTRAP:20

for b₁ being RealLinearSpace
for b₂, b₃, b₄, b₅, b₆ being VECTOR of b₁ st Gen b₂,b₃ & b₄,b₅,b₅,b₆ are_DTr_wrt b₂,b₃ holds
( b₄ = b₅ & b₅ = b₆ )

proof end;

theorem Th21: :: GEOMTRAP:21

for b₁ being RealLinearSpace
for b₂, b₃, b₄, b₅, b₆, b₇, b₈, b₉ being VECTOR of b₁ st Gen b₂,b₃ & b₄,b₅,b₆,b₇ are_DTr_wrt b₂,b₃ & b₄,b₅,b₈,b₉ are_DTr_wrt b₂,b₃ & b₄ <> b₅ holds
b₆,b₇,b₈,b₉ are_DTr_wrt b₂,b₃

proof end;

theorem Th22: :: GEOMTRAP:22

for b₁ being RealLinearSpace
for b₂, b₃, b₄, b₅, b₆ being VECTOR of b₁ st Gen b₂,b₃ holds
ex b₇ being VECTOR of b₁ st
( b₄,b₅,b₆,b₇ are_DTr_wrt b₂,b₃ or b₄,b₅,b₇,b₆ are_DTr_wrt b₂,b₃ )

proof end;

theorem Th23: :: GEOMTRAP:23

for b₁ being RealLinearSpace
for b₂, b₃, b₄, b₅, b₆, b₇ being VECTOR of b₁ st Gen b₂,b₃ & b₄,b₅,b₆,b₇ are_DTr_wrt b₂,b₃ holds
b₆,b₇,b₄,b₅ are_DTr_wrt b₂,b₃

proof end;

theorem Th24: :: GEOMTRAP:24

for b₁ being RealLinearSpace
for b₂, b₃, b₄, b₅, b₆, b₇ being VECTOR of b₁ st Gen b₂,b₃ & b₄,b₅,b₆,b₇ are_DTr_wrt b₂,b₃ holds
b₅,b₄,b₇,b₆ are_DTr_wrt b₂,b₃

proof end;

Lemma32: for b₁ being RealLinearSpace
for b₂, b₃, b₄, b₅, b₆, b₇, b₈, b₉ being VECTOR of b₁ st Gen b₂,b₃ & b₄ <> b₅ & b₄,b₅ '||' b₄,b₆ & b₄,b₅ '||' b₄,b₇ & b₄,b₅ '||' b₄,b₈ & b₄,b₅ '||' b₄,b₉ holds
b₆,b₇ '||' b₈,b₉

proof end;

theorem Th25: :: GEOMTRAP:25

for b₁ being RealLinearSpace
for b₂, b₃, b₄, b₅, b₆ being VECTOR of b₁ st Gen b₂,b₃ & b₄,b₅,b₄,b₆ are_DTr_wrt b₂,b₃ holds
b₅ = b₆

proof end;

theorem Th26: :: GEOMTRAP:26

for b₁ being RealLinearSpace
for b₂, b₃, b₄, b₅, b₆, b₇, b₈ being VECTOR of b₁ st Gen b₂,b₃ & b₄,b₅,b₆,b₇ are_DTr_wrt b₂,b₃ & b₄,b₅,b₆,b₈ are_DTr_wrt b₂,b₃ & not b₄ = b₅ holds
b₇ = b₈

proof end;

theorem Th27: :: GEOMTRAP:27

for b₁ being RealLinearSpace
for b₂, b₃, b₄, b₅, b₆, b₇, b₈ being VECTOR of b₁ st Gen b₂,b₃ & b₄ <> b₅ & b₄,b₅,b₆,b₇ are_DTr_wrt b₂,b₃ & ( b₄,b₅,b₆,b₈ are_DTr_wrt b₂,b₃ or b₄,b₅,b₈,b₆ are_DTr_wrt b₂,b₃ ) holds
b₇ = b₈

proof end;

theorem Th28: :: GEOMTRAP:28

for b₁ being RealLinearSpace
for b₂, b₃, b₄, b₅, b₆, b₇ being VECTOR of b₁ st Gen b₂,b₃ & b₄,b₅,b₆,b₇ are_DTr_wrt b₂,b₃ holds
b₄,b₅,b₄ # b₆,b₅ # b₇ are_DTr_wrt b₂,b₃

proof end;

theorem Th29: :: GEOMTRAP:29

for b₁ being RealLinearSpace
for b₂, b₃, b₄, b₅, b₆, b₇ being VECTOR of b₁ st Gen b₂,b₃ & b₄,b₅,b₆,b₇ are_DTr_wrt b₂,b₃ & not b₄,b₅,b₄ # b₇,b₅ # b₆ are_DTr_wrt b₂,b₃ holds
b₄,b₅,b₅ # b₆,b₄ # b₇ are_DTr_wrt b₂,b₃

proof end;

theorem Th30: :: GEOMTRAP:30

for b₁ being RealLinearSpace
for b₂, b₃, b₄, b₅, b₆, b₇, b₈, b₉, b₁₀, b₁₁, b₁₂ being VECTOR of b₁ st Gen b₂,b₃ & b₄ = b₅ # b₉ & b₄ = b₆ # b₁₀ & b₄ = b₇ # b₁₁ & b₄ = b₈ # b₁₂ & b₅,b₆,b₇,b₈ are_DTr_wrt b₂,b₃ holds
b₉,b₁₀,b₁₁,b₁₂ are_DTr_wrt b₂,b₃

proof end;

Lemma39: for b₁ being RealLinearSpace
for b₂, b₃, b₄, b₅ being VECTOR of b₁
for b₆, b₇, b₈, b₉ being Real st b₂ = (b₆ * b₃) + (b₇ * b₄) & b₅ = (b₈ * b₃) + (b₉ * b₄) holds
( b₂ + b₅ = ((b₆ + b₈) * b₃) + ((b₇ + b₉) * b₄) & b₂ - b₅ = ((b₆ - b₈) * b₃) + ((b₇ - b₉) * b₄) )

proof end;

Lemma40: for b₁ being RealLinearSpace
for b₂, b₃, b₄ being VECTOR of b₁
for b₅, b₆, b₇ being Real st b₂ = (b₅ * b₃) + (b₆ * b₄) holds
b₇ * b₂ = ((b₇ * b₅) * b₃) + ((b₇ * b₆) * b₄)

proof end;

Lemma41: for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁
for b₄, b₅, b₆, b₇ being Real st Gen b₂,b₃ & (b₄ * b₂) + (b₅ * b₃) = (b₆ * b₂) + (b₇ * b₃) holds
( b₄ = b₆ & b₅ = b₇ )

proof end;

definition

let c₁ be RealLinearSpace;
let c₂, c₃, c₄ be VECTOR of c₁;
assume E42: Gen c₂,c₃ ;
func pr1 c₂,c₃,c₄ -> Real means :Def4: :: GEOMTRAP:def 4
ex b₁ being Real st a₄ = (a₅ * a₂) + (b₁ * a₃);
existence by E42, ANALMETR:def 1;
uniqueness by E42, Lemma41;

end;

:: deftheorem Def4 defines pr1 GEOMTRAP:def 4 :

definition

let c₁ be RealLinearSpace;
let c₂, c₃, c₄ be VECTOR of c₁;
assume E43: Gen c₂,c₃ ;
func pr2 c₂,c₃,c₄ -> Real means :Def5: :: GEOMTRAP:def 5
ex b₁ being Real st a₄ = (b₁ * a₂) + (a₅ * a₃);
existence

proof end;

uniqueness by E43, Lemma41;

end;

:: deftheorem Def5 defines pr2 GEOMTRAP:def 5 :

Lemma44: for b₁ being RealLinearSpace
for b₂, b₃, b₄ being VECTOR of b₁ st Gen b₂,b₃ holds
b₄ = ((pr1 b₂,b₃,b₄) * b₂) + ((pr2 b₂,b₃,b₄) * b₃)

proof end;

Lemma45: for b₁ being RealLinearSpace
for b₂, b₃, b₄ being VECTOR of b₁
for b₅, b₆ being Real st Gen b₂,b₃ & b₄ = (b₅ * b₂) + (b₆ * b₃) holds
( b₅ = pr1 b₂,b₃,b₄ & b₆ = pr2 b₂,b₃,b₄ )

proof end;

Lemma46: for b₁ being RealLinearSpace
for b₂, b₃, b₄, b₅ being VECTOR of b₁
for b₆ being Real st Gen b₂,b₃ holds
( pr1 b₂,b₃,(b₄ + b₅) = (pr1 b₂,b₃,b₄) + (pr1 b₂,b₃,b₅) & pr2 b₂,b₃,(b₄ + b₅) = (pr2 b₂,b₃,b₄) + (pr2 b₂,b₃,b₅) & pr1 b₂,b₃,(b₄ - b₅) = (pr1 b₂,b₃,b₄) - (pr1 b₂,b₃,b₅) & pr2 b₂,b₃,(b₄ - b₅) = (pr2 b₂,b₃,b₄) - (pr2 b₂,b₃,b₅) & pr1 b₂,b₃,(b₆ * b₄) = b₆ * (pr1 b₂,b₃,b₄) & pr2 b₂,b₃,(b₆ * b₄) = b₆ * (pr2 b₂,b₃,b₄) )

proof end;

Lemma47: for b₁ being RealLinearSpace
for b₂, b₃, b₄, b₅ being VECTOR of b₁ st Gen b₂,b₃ holds
( 2 * (pr1 b₂,b₃,(b₄ # b₅)) = (pr1 b₂,b₃,b₄) + (pr1 b₂,b₃,b₅) & 2 * (pr2 b₂,b₃,(b₄ # b₅)) = (pr2 b₂,b₃,b₄) + (pr2 b₂,b₃,b₅) )

proof end;

Lemma48: for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁ holds (- b₂) + (- b₃) = - (b₂ + b₃)

proof end;

Lemma49: for b₁ being RealLinearSpace
for b₂, b₃, b₄ being VECTOR of b₁
for b₅, b₆ being Real holds (b₂ + (b₅ * b₃)) - (b₄ + (b₆ * b₃)) = (b₂ - b₄) + ((b₅ - b₆) * b₃)

proof end;

definition

let c₁ be RealLinearSpace;
let c₂, c₃, c₄, c₅ be VECTOR of c₁;
func PProJ c₂,c₃,c₄,c₅ -> Real equals :: GEOMTRAP:def 6
((pr1 a₂,a₃,a₄) * (pr1 a₂,a₃,a₅)) + ((pr2 a₂,a₃,a₄) * (pr2 a₂,a₃,a₅));
correctness ;

end;

:: deftheorem Def6 defines PProJ GEOMTRAP:def 6 :

theorem Th31: :: GEOMTRAP:31

for b₁ being RealLinearSpace
for b₂, b₃, b₄, b₅ being VECTOR of b₁ holds PProJ b₂,b₃,b₄,b₅ = PProJ b₂,b₃,b₅,b₄ ;

theorem Th32: :: GEOMTRAP:32

for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁ st Gen b₂,b₃ holds
for b₄, b₅, b₆ being VECTOR of b₁ holds
( PProJ b₂,b₃,b₄,(b₅ + b₆) = (PProJ b₂,b₃,b₄,b₅) + (PProJ b₂,b₃,b₄,b₆) & PProJ b₂,b₃,b₄,(b₅ - b₆) = (PProJ b₂,b₃,b₄,b₅) - (PProJ b₂,b₃,b₄,b₆) & PProJ b₂,b₃,(b₅ - b₆),b₄ = (PProJ b₂,b₃,b₅,b₄) - (PProJ b₂,b₃,b₆,b₄) & PProJ b₂,b₃,(b₅ + b₆),b₄ = (PProJ b₂,b₃,b₅,b₄) + (PProJ b₂,b₃,b₆,b₄) )

proof end;

theorem Th33: :: GEOMTRAP:33

for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁ st Gen b₂,b₃ holds
for b₄, b₅ being VECTOR of b₁
for b₆ being Real holds
( PProJ b₂,b₃,(b₆ * b₄),b₅ = b₆ * (PProJ b₂,b₃,b₄,b₅) & PProJ b₂,b₃,b₄,(b₆ * b₅) = b₆ * (PProJ b₂,b₃,b₄,b₅) & PProJ b₂,b₃,(b₆ * b₄),b₅ = (PProJ b₂,b₃,b₄,b₅) * b₆ & PProJ b₂,b₃,b₄,(b₆ * b₅) = (PProJ b₂,b₃,b₄,b₅) * b₆ )

proof end;

theorem Th34: :: GEOMTRAP:34

for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁ st Gen b₂,b₃ holds
for b₄, b₅ being VECTOR of b₁ holds
( b₄,b₅ are_Ort_wrt b₂,b₃ iff PProJ b₂,b₃,b₄,b₅ = 0 )

proof end;

theorem Th35: :: GEOMTRAP:35

for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁ st Gen b₂,b₃ holds
for b₄, b₅, b₆, b₇ being VECTOR of b₁ holds
( b₄,b₅,b₆,b₇ are_Ort_wrt b₂,b₃ iff PProJ b₂,b₃,(b₅ - b₄),(b₇ - b₆) = 0 )

proof end;

theorem Th36: :: GEOMTRAP:36

for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁ st Gen b₂,b₃ holds
for b₄, b₅, b₆ being VECTOR of b₁ holds 2 * (PProJ b₂,b₃,b₄,(b₅ # b₆)) = (PProJ b₂,b₃,b₄,b₅) + (PProJ b₂,b₃,b₄,b₆)

proof end;

theorem Th37: :: GEOMTRAP:37

for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁ st Gen b₂,b₃ holds
for b₄, b₅ being VECTOR of b₁ st b₄ <> b₅ holds
PProJ b₂,b₃,(b₄ - b₅),(b₄ - b₅) <> 0

proof end;

theorem Th38: :: GEOMTRAP:38

for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁ st Gen b₂,b₃ holds
for b₄, b₅, b₆, b₇, b₈ being VECTOR of b₁
for b₉ being Real st b₄,b₅,b₆,b₇ are_DTr_wrt b₂,b₃ & b₄ <> b₅ & b₉ = ((PProJ b₂,b₃,(b₄ - b₅),(b₄ + b₅)) - (2 * (PProJ b₂,b₃,(b₄ - b₅),b₆))) * ((PProJ b₂,b₃,(b₄ - b₅),(b₄ - b₅)) " ) & b₈ = b₆ + (b₉ * (b₄ - b₅)) holds
b₇ = b₈

proof end;

Lemma57: for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁ st Gen b₂,b₃ holds
for b₄, b₅, b₆, b₇, b₈, b₉ being VECTOR of b₁
for b₁₀, b₁₁ being Real st b₄ <> b₅ & b₁₀ = ((PProJ b₂,b₃,(b₄ - b₅),(b₄ + b₅)) - (2 * (PProJ b₂,b₃,(b₄ - b₅),b₆))) * ((PProJ b₂,b₃,(b₄ - b₅),(b₄ - b₅)) " ) & b₁₁ = ((PProJ b₂,b₃,(b₄ - b₅),(b₄ + b₅)) - (2 * (PProJ b₂,b₃,(b₄ - b₅),b₇))) * ((PProJ b₂,b₃,(b₄ - b₅),(b₄ - b₅)) " ) & b₈ = b₆ + (b₁₀ * (b₄ - b₅)) & b₉ = b₇ + (b₁₁ * (b₄ - b₅)) holds
( b₉ - b₈ = (b₇ - b₆) + ((b₁₁ - b₁₀) * (b₄ - b₅)) & b₁₁ - b₁₀ = ((- 2) * (PProJ b₂,b₃,(b₄ - b₅),(b₇ - b₆))) * ((PProJ b₂,b₃,(b₄ - b₅),(b₄ - b₅)) " ) )

proof end;

theorem Th39: :: GEOMTRAP:39

for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁ st Gen b₂,b₃ holds
for b₄, b₅, b₆, b₇, b₈, b₉, b₁₀, b₁₁, b₁₂, b₁₃ being VECTOR of b₁ st b₄ <> b₅ & b₄,b₅,b₆,b₁₀ are_DTr_wrt b₂,b₃ & b₄,b₅,b₇,b₁₁ are_DTr_wrt b₂,b₃ & b₄,b₅,b₈,b₁₂ are_DTr_wrt b₂,b₃ & b₄,b₅,b₉,b₁₃ are_DTr_wrt b₂,b₃ & b₆,b₇ // b₈,b₉ holds
b₁₀,b₁₁ // b₁₂,b₁₃

proof end;

theorem Th40: :: GEOMTRAP:40

for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁ st Gen b₂,b₃ holds
for b₄, b₅, b₆, b₇, b₈, b₉, b₁₀, b₁₁ being VECTOR of b₁ st b₄ <> b₅ & b₄,b₅,b₆,b₉ are_DTr_wrt b₂,b₃ & b₄,b₅,b₇,b₁₀ are_DTr_wrt b₂,b₃ & b₄,b₅,b₈,b₁₁ are_DTr_wrt b₂,b₃ & b₈ = b₆ # b₇ holds
b₁₁ = b₉ # b₁₀

proof end;

theorem Th41: :: GEOMTRAP:41

for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁ st Gen b₂,b₃ holds
for b₄, b₅, b₆, b₇, b₈, b₉ being VECTOR of b₁ st b₄ <> b₅ & b₄,b₅,b₆,b₈ are_DTr_wrt b₂,b₃ & b₄,b₅,b₇,b₉ are_DTr_wrt b₂,b₃ holds
b₄,b₅,b₆ # b₇,b₈ # b₉ are_DTr_wrt b₂,b₃

proof end;

theorem Th42: :: GEOMTRAP:42

for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁ st Gen b₂,b₃ holds
for b₄, b₅, b₆, b₇, b₈, b₉, b₁₀, b₁₁, b₁₂, b₁₃ being VECTOR of b₁ st b₄ <> b₅ & b₄,b₅,b₆,b₁₀ are_DTr_wrt b₂,b₃ & b₄,b₅,b₇,b₁₁ are_DTr_wrt b₂,b₃ & b₄,b₅,b₈,b₁₂ are_DTr_wrt b₂,b₃ & b₄,b₅,b₉,b₁₃ are_DTr_wrt b₂,b₃ & b₆,b₇,b₈,b₉ are_Ort_wrt b₂,b₃ holds
b₁₀,b₁₁,b₁₂,b₁₃ are_Ort_wrt b₂,b₃

proof end;

theorem Th43: :: GEOMTRAP:43

for b₁ being RealLinearSpace
for b₂, b₃, b₄, b₅, b₆, b₇, b₈, b₉, b₁₀, b₁₁, b₁₂, b₁₃ being VECTOR of b₁ st Gen b₂,b₃ & b₄ <> b₅ & b₄,b₅,b₆,b₁₀ are_DTr_wrt b₂,b₃ & b₄,b₅,b₇,b₁₁ are_DTr_wrt b₂,b₃ & b₄,b₅,b₈,b₁₂ are_DTr_wrt b₂,b₃ & b₄,b₅,b₉,b₁₃ are_DTr_wrt b₂,b₃ & b₆,b₇,b₈,b₉ are_DTr_wrt b₂,b₃ holds
b₁₀,b₁₁,b₁₂,b₁₃ are_DTr_wrt b₂,b₃

proof end;

definition

let c₁ be RealLinearSpace;
let c₂, c₃ be VECTOR of c₁;
func DTrapezium c₁,c₂,c₃ -> Relation of [:the carrier of a₁,the carrier of a₁:] means :Def7: :: GEOMTRAP:def 7
for b₁, b₂ being set holds
( [b₁,b₂] in a₄ iff ex b₃, b₄, b₅, b₆ being VECTOR of a₁ st
( b₁ = [b₃,b₄] & b₂ = [b₅,b₆] & b₃,b₄,b₅,b₆ are_DTr_wrt a₂,a₃ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines DTrapezium GEOMTRAP:def 7 :

theorem Th44: :: GEOMTRAP:44

for b₁ being RealLinearSpace
for b₂, b₃, b₄, b₅, b₆, b₇ being VECTOR of b₁ holds
( [[b₂,b₃],[b₄,b₅]] in DTrapezium b₁,b₆,b₇ iff b₂,b₃,b₄,b₅ are_DTr_wrt b₆,b₇ )

proof end;

definition

let c₁ be RealLinearSpace;
func MidPoint c₁ -> BinOp of the carrier of a₁ means :Def8: :: GEOMTRAP:def 8
for b₁, b₂ being VECTOR of a₁ holds a₂ . b₁,b₂ = b₁ # b₂;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines MidPoint GEOMTRAP:def 8 :

definition

attr a₁ is strict;
struct AfMidStruct -> AffinStruct , MidStr ;
aggr AfMidStruct(# carrier, MIDPOINT, CONGR #) -> AfMidStruct ;

end;

registration

cluster non empty strict AfMidStruct ;
existence

proof end;

end;

definition

let c₁ be RealLinearSpace;
let c₂, c₃ be VECTOR of c₁;
func DTrSpace c₁,c₂,c₃ -> strict AfMidStruct equals :: GEOMTRAP:def 9
AfMidStruct(# the carrier of a₁,(MidPoint a₁),(DTrapezium a₁,a₂,a₃) #);
correctness ;

end;

:: deftheorem Def9 defines DTrSpace GEOMTRAP:def 9 :

registration

let c₁ be RealLinearSpace;
let c₂, c₃ be VECTOR of c₁;
cluster DTrSpace a₁,a₂,a₃ -> non empty strict ;
coherence

proof end;

end;

definition

let c₁ be AfMidStruct ;
func Af c₁ -> strict AffinStruct equals :: GEOMTRAP:def 10
AffinStruct(# the carrier of a₁,the CONGR of a₁ #);
correctness ;

end;

:: deftheorem Def10 defines Af GEOMTRAP:def 10 :

registration

let c₁ be non empty AfMidStruct ;
cluster Af a₁ -> non empty strict ;
coherence

proof end;

end;

definition

let c₁ be non empty AfMidStruct ;
let c₂, c₃ be Element of c₁;
canceled;
func c₂ # c₃ -> Element of a₁ equals :: GEOMTRAP:def 12
the MIDPOINT of a₁ . a₂,a₃;
correctness ;

end;

:: deftheorem Def11 GEOMTRAP:def 11 :

:: deftheorem Def12 defines # GEOMTRAP:def 12 :

theorem Th45: :: GEOMTRAP:45

canceled;

theorem Th46: :: GEOMTRAP:46

for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁
for b₄ being set holds
( b₄ is Element of the carrier of (DTrSpace b₁,b₂,b₃) iff b₄ is VECTOR of b₁ ) ;

theorem Th47: :: GEOMTRAP:47

for b₁ being RealLinearSpace
for b₂, b₃, b₄, b₅, b₆, b₇ being VECTOR of b₁
for b₈, b₉, b₁₀, b₁₁ being Element of (DTrSpace b₁,b₂,b₃) st Gen b₂,b₃ & b₄ = b₈ & b₅ = b₉ & b₆ = b₁₀ & b₇ = b₁₁ holds
( b₈,b₉ // b₁₀,b₁₁ iff b₄,b₅,b₆,b₇ are_DTr_wrt b₂,b₃ )

proof end;

theorem Th48: :: GEOMTRAP:48

for b₁ being RealLinearSpace
for b₂, b₃, b₄, b₅ being VECTOR of b₁
for b₆, b₇ being Element of (DTrSpace b₁,b₂,b₃) st Gen b₂,b₃ & b₄ = b₆ & b₅ = b₇ holds
b₄ # b₅ = b₆ # b₇ by Def8;

Lemma67: for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁
for b₄, b₅, b₆ being Element of (DTrSpace b₁,b₂,b₃) st Gen b₂,b₃ & b₄,b₅ // b₅,b₆ holds
( b₄ = b₅ & b₅ = b₆ )

proof end;

Lemma68: for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁
for b₄, b₅, b₆, b₇, b₈, b₉ being Element of (DTrSpace b₁,b₂,b₃) st Gen b₂,b₃ & b₄,b₅ // b₆,b₇ & b₄,b₅ // b₈,b₉ & b₄ <> b₅ holds
b₆,b₇ // b₈,b₉

proof end;

Lemma69: for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁
for b₄, b₅, b₆, b₇ being Element of (DTrSpace b₁,b₂,b₃) st Gen b₂,b₃ & b₄,b₅ // b₆,b₇ holds
( b₆,b₇ // b₄,b₅ & b₅,b₄ // b₇,b₆ )

proof end;

Lemma70: for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁
for b₄, b₅, b₆ being Element of (DTrSpace b₁,b₂,b₃) st Gen b₂,b₃ holds
ex b₇ being Element of (DTrSpace b₁,b₂,b₃) st
( b₄,b₅ // b₆,b₇ or b₄,b₅ // b₇,b₆ )

proof end;

Lemma71: for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁
for b₄, b₅, b₆, b₇, b₈ being Element of (DTrSpace b₁,b₂,b₃) st Gen b₂,b₃ & b₄,b₅ // b₆,b₇ & b₄,b₅ // b₆,b₈ & not b₄ = b₅ holds
b₇ = b₈

proof end;

Lemma72: for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁
for b₄, b₅ being Element of (DTrSpace b₁,b₂,b₃) st Gen b₂,b₃ holds
b₄ # b₅ = b₅ # b₄

proof end;

Lemma73: for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁
for b₄ being Element of (DTrSpace b₁,b₂,b₃) st Gen b₂,b₃ holds
b₄ # b₄ = b₄

proof end;

Lemma74: for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁
for b₄, b₅, b₆, b₇ being Element of (DTrSpace b₁,b₂,b₃) st Gen b₂,b₃ holds
(b₄ # b₅) # (b₆ # b₇) = (b₄ # b₆) # (b₅ # b₇)

proof end;

Lemma75: for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁
for b₄, b₅ being Element of (DTrSpace b₁,b₂,b₃) st Gen b₂,b₃ holds
ex b₆ being Element of (DTrSpace b₁,b₂,b₃) st b₆ # b₄ = b₅

proof end;

Lemma76: for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁
for b₄, b₅, b₆ being Element of (DTrSpace b₁,b₂,b₃) st Gen b₂,b₃ & b₄ # b₅ = b₄ # b₆ holds
b₅ = b₆

proof end;

Lemma77: for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁
for b₄, b₅, b₆, b₇ being Element of (DTrSpace b₁,b₂,b₃) st Gen b₂,b₃ & b₄,b₅ // b₆,b₇ holds
b₄,b₅ // b₄ # b₆,b₅ # b₇

proof end;

Lemma78: for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁
for b₄, b₅, b₆, b₇ being Element of (DTrSpace b₁,b₂,b₃) st Gen b₂,b₃ & b₄,b₅ // b₆,b₇ & not b₄,b₅ // b₄ # b₇,b₅ # b₆ holds
b₄,b₅ // b₅ # b₆,b₄ # b₇

proof end;

Lemma79: for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁
for b₄, b₅, b₆, b₇, b₈, b₉, b₁₀, b₁₁, b₁₂ being Element of (DTrSpace b₁,b₂,b₃) st Gen b₂,b₃ & b₄,b₅ // b₆,b₇ & b₄ # b₈ = b₉ & b₅ # b₁₀ = b₉ & b₆ # b₁₁ = b₉ & b₇ # b₁₂ = b₉ holds
b₈,b₁₀ // b₁₁,b₁₂

proof end;

Lemma80: for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁
for b₄, b₅, b₆, b₇, b₈, b₉, b₁₀, b₁₁, b₁₂, b₁₃ being Element of (DTrSpace b₁,b₂,b₃) st Gen b₂,b₃ & b₄ <> b₅ & b₄,b₅ // b₆,b₇ & b₄,b₅ // b₈,b₉ & b₄,b₅ // b₁₀,b₁₁ & b₄,b₅ // b₁₂,b₁₃ & b₆,b₈ // b₁₀,b₁₂ holds
b₇,b₉ // b₁₁,b₁₃

proof end;

definition

let c₁ be non empty AfMidStruct ;
attr a₁ is MidOrdTrapSpace-like means :Def13: :: GEOMTRAP:def 13
for b₁, b₂, b₃, b₄, b₅, b₆, b₇, b₈, b₉, b₁₀ being Element of a₁ holds
( b₁ # b₂ = b₂ # b₁ & b₁ # b₁ = b₁ & (b₁ # b₂) # (b₃ # b₄) = (b₁ # b₃) # (b₂ # b₄) & ex b₁₁ being Element of a₁ st b₁₁ # b₁ = b₂ & ( b₁ # b₂ = b₁ # b₃ implies b₂ = b₃ ) & ( b₁,b₂ // b₃,b₄ implies b₁,b₂ // b₁ # b₃,b₂ # b₄ ) & ( not b₁,b₂ // b₃,b₄ or b₁,b₂ // b₁ # b₄,b₂ # b₃ or b₁,b₂ // b₂ # b₃,b₁ # b₄ ) & ( b₁,b₂ // b₃,b₄ & b₁ # b₅ = b₉ & b₂ # b₆ = b₉ & b₃ # b₇ = b₉ & b₄ # b₈ = b₉ implies b₅,b₆ // b₇,b₈ ) & ( b₉ <> b₁₀ & b₉,b₁₀ // b₁,b₅ & b₉,b₁₀ // b₂,b₆ & b₉,b₁₀ // b₃,b₇ & b₉,b₁₀ // b₄,b₈ & b₁,b₂ // b₃,b₄ implies b₅,b₆ // b₇,b₈ ) & ( b₁,b₂ // b₂,b₃ implies ( b₁ = b₂ & b₂ = b₃ ) ) & ( b₁,b₂ // b₅,b₆ & b₁,b₂ // b₇,b₈ & b₁ <> b₂ implies b₅,b₆ // b₇,b₈ ) & ( b₁,b₂ // b₃,b₄ implies ( b₃,b₄ // b₁,b₂ & b₂,b₁ // b₄,b₃ ) ) & ex b₁₁ being Element of a₁ st
( b₁,b₂ // b₃,b₁₁ or b₁,b₂ // b₁₁,b₃ ) & ( b₁,b₂ // b₃,b₉ & b₁,b₂ // b₃,b₁₀ & not b₁ = b₂ implies b₉ = b₁₀ ) );

end;

:: deftheorem Def13 defines MidOrdTrapSpace-like GEOMTRAP:def 13 :

registration

cluster non empty strict MidOrdTrapSpace-like AfMidStruct ;
existence

proof end;

end;

definition

mode MidOrdTrapSpace is non empty MidOrdTrapSpace-like AfMidStruct ;

end;

theorem Th49: :: GEOMTRAP:49

for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁ st Gen b₂,b₃ holds
DTrSpace b₁,b₂,b₃ is MidOrdTrapSpace

proof end;

consider c₁ being MidOrdTrapSpace;

set c₂ = Af c₁;

E82: now

let c₃, c₄, c₅, c₆, c₇, c₈, c₉, c₁₀, c₁₁, c₁₂ be Element of (Af c₁);

E83: now

let c₁₃, c₁₄, c₁₅, c₁₆ be Element of (Af c₁);
let c₁₇, c₁₈, c₁₉, c₂₀ be Element of the carrier of c₁;
assume E84: ( c₁₃ = c₁₇ & c₁₄ = c₁₈ & c₁₅ = c₁₉ & c₁₆ = c₂₀ ) ;

E85: now

assume c₁₃,c₁₄ // c₁₅,c₁₆ ;
then [[c₁₃,c₁₄],[c₁₅,c₁₆]] in the CONGR of c₁ by ANALOAF:def 2;
hence c₁₇,c₁₈ // c₁₉,c₂₀ by E84, ANALOAF:def 2;

end;

now

assume c₁₇,c₁₈ // c₁₉,c₂₀ ;
then [[c₁₃,c₁₄],[c₁₅,c₁₆]] in the CONGR of c₁ by E84, ANALOAF:def 2;
hence c₁₃,c₁₄ // c₁₅,c₁₆ by ANALOAF:def 2;

end;

hence ( c₁₃,c₁₄ // c₁₅,c₁₆ iff c₁₇,c₁₈ // c₁₉,c₂₀ ) by E85;

end;

reconsider c₁₃ = c₃, c₁₄ = c₄, c₁₅ = c₅, c₁₆ = c₆, c₁₇ = c₇, c₁₈ = c₈, c₁₉ = c₉, c₂₀ = c₁₀, c₂₁ = c₁₁, c₂₂ = c₁₂ as Element of c₁ ;

E84: now

assume c₃,c₄ // c₄,c₅ ;
then c₁₃,c₁₄ // c₁₄,c₁₅ by E83;
hence ( c₃ = c₄ & c₄ = c₅ ) by Def13;

end;

E85: now

assume ( c₃,c₄ // c₇,c₈ & c₃,c₄ // c₉,c₁₀ & c₃ <> c₄ ) ;
then ( c₁₃,c₁₄ // c₁₇,c₁₈ & c₁₃,c₁₄ // c₁₉,c₂₀ & c₁₃ <> c₁₄ ) by E83;
then c₁₇,c₁₈ // c₁₉,c₂₀ by Def13;
hence c₇,c₈ // c₉,c₁₀ by E83;

end;

E86: now

assume c₃,c₄ // c₅,c₆ ;
then c₁₃,c₁₄ // c₁₅,c₁₆ by E83;
then ( c₁₅,c₁₆ // c₁₃,c₁₄ & c₁₄,c₁₃ // c₁₆,c₁₅ ) by Def13;
hence ( c₅,c₆ // c₃,c₄ & c₄,c₃ // c₆,c₅ ) by E83;

end;

E87: ex b₁ being Element of (Af c₁) st
( c₃,c₄ // c₅,b₁ or c₃,c₄ // b₁,c₅ )

proof

consider c₂₃ being Element of c₁ such that
E88: ( c₁₃,c₁₄ // c₁₅,c₂₃ or c₁₃,c₁₄ // c₂₃,c₁₅ ) by Def13;
reconsider c₂₄ = c₂₃ as Element of (Af c₁) ;
take c₂₄ ;
thus ( c₃,c₄ // c₅,c₂₄ or c₃,c₄ // c₂₄,c₅ ) by E83, E88;

end;

now

assume ( c₃,c₄ // c₅,c₁₁ & c₃,c₄ // c₅,c₁₂ ) ;
then ( c₁₃,c₁₄ // c₁₅,c₂₁ & c₁₃,c₁₄ // c₁₅,c₂₂ ) by E83;
hence ( c₃ = c₄ or c₁₁ = c₁₂ ) by Def13;

end;

hence ( ( c₃,c₄ // c₄,c₅ implies ( c₃ = c₄ & c₄ = c₅ ) ) & ( c₃,c₄ // c₇,c₈ & c₃,c₄ // c₉,c₁₀ & c₃ <> c₄ implies c₇,c₈ // c₉,c₁₀ ) & ( c₃,c₄ // c₅,c₆ implies ( c₅,c₆ // c₃,c₄ & c₄,c₃ // c₆,c₅ ) ) & ex b₁ being Element of (Af c₁) st
( c₃,c₄ // c₅,b₁ or c₃,c₄ // b₁,c₅ ) & ( c₃,c₄ // c₅,c₁₁ & c₃,c₄ // c₅,c₁₂ & not c₃ = c₄ implies c₁₁ = c₁₂ ) ) by E84, E85, E86, E87;

end;

definition

let c₃ be non empty AffinStruct ;
attr a₁ is OrdTrapSpace-like means :Def14: :: GEOMTRAP:def 14
for b₁, b₂, b₃, b₄, b₅, b₆, b₇, b₈, b₉, b₁₀ being Element of a₁ holds
( ( b₁,b₂ // b₂,b₃ implies ( b₁ = b₂ & b₂ = b₃ ) ) & ( b₁,b₂ // b₅,b₆ & b₁,b₂ // b₇,b₈ & b₁ <> b₂ implies b₅,b₆ // b₇,b₈ ) & ( b₁,b₂ // b₃,b₄ implies ( b₃,b₄ // b₁,b₂ & b₂,b₁ // b₄,b₃ ) ) & ex b₁₁ being Element of a₁ st
( b₁,b₂ // b₃,b₁₁ or b₁,b₂ // b₁₁,b₃ ) & ( b₁,b₂ // b₃,b₉ & b₁,b₂ // b₃,b₁₀ & not b₁ = b₂ implies b₉ = b₁₀ ) );

end;

:: deftheorem Def14 defines OrdTrapSpace-like GEOMTRAP:def 14 :

registration

cluster non empty strict OrdTrapSpace-like AffinStruct ;
existence

proof end;

end;

definition

mode OrdTrapSpace is non empty OrdTrapSpace-like AffinStruct ;

end;

registration

let c₃ be MidOrdTrapSpace;
cluster Af a₁ -> non empty strict OrdTrapSpace-like ;
coherence

proof end;

end;

theorem Th50: :: GEOMTRAP:50

for b₁ being OrdTrapSpace
for b₂ being set holds
( b₂ is Element of b₁ iff b₂ is Element of (Lambda b₁) )

proof end;

theorem Th51: :: GEOMTRAP:51

for b₁ being OrdTrapSpace
for b₂, b₃, b₄, b₅ being Element of b₁
for b₆, b₇, b₈, b₉ being Element of (Lambda b₁) st b₂ = b₆ & b₃ = b₇ & b₄ = b₈ & b₅ = b₉ holds
( b₆,b₇ // b₈,b₉ iff ( b₂,b₃ // b₄,b₅ or b₂,b₃ // b₅,b₄ ) )

proof end;

Lemma86: for b₁ being OrdTrapSpace
for b₂, b₃, b₄ being Element of (Lambda b₁) ex b₅ being Element of (Lambda b₁) st b₂,b₃ // b₄,b₅

proof end;

Lemma87: for b₁ being OrdTrapSpace
for b₂, b₃, b₄, b₅ being Element of (Lambda b₁) st b₂,b₃ // b₄,b₅ holds
b₄,b₅ // b₂,b₃

proof end;

Lemma88: for b₁ being OrdTrapSpace
for b₂, b₃, b₄, b₅, b₆, b₇ being Element of (Lambda b₁) st b₂ <> b₃ & b₂,b₃ // b₄,b₅ & b₂,b₃ // b₆,b₇ holds
b₄,b₅ // b₆,b₇

proof end;

Lemma89: for b₁ being OrdTrapSpace
for b₂, b₃, b₄, b₅, b₆ being Element of (Lambda b₁) st b₂,b₃ // b₄,b₅ & b₂,b₃ // b₄,b₆ & not b₂ = b₃ holds
b₅ = b₆

proof end;

Lemma90: for b₁ being OrdTrapSpace
for b₂, b₃ being Element of b₁ holds b₂,b₃ // b₂,b₃

proof end;

Lemma91: for b₁ being OrdTrapSpace
for b₂, b₃ being Element of (Lambda b₁) holds b₂,b₃ // b₃,b₂

proof end;

definition

let c₃ be non empty AffinStruct ;
attr a₁ is TrapSpace-like means :Def15: :: GEOMTRAP:def 15
for b₁, b₂, b₃, b₄, b₅, b₆ being Element of a₁ holds
( b₁,b₂ // b₂,b₁ & ( b₁,b₂ // b₃,b₄ & b₁,b₂ // b₃,b₆ & not b₁ = b₂ implies b₄ = b₆ ) & ( b₅ <> b₆ & b₅,b₆ // b₁,b₂ & b₅,b₆ // b₃,b₄ implies b₁,b₂ // b₃,b₄ ) & ( b₁,b₂ // b₃,b₄ implies b₃,b₄ // b₁,b₂ ) & ex b₇ being Element of a₁ st b₁,b₂ // b₃,b₇ );

end;

:: deftheorem Def15 defines TrapSpace-like GEOMTRAP:def 15 :

registration

cluster non empty strict TrapSpace-like AffinStruct ;
existence

proof end;

end;

definition

mode TrapSpace is non empty TrapSpace-like AffinStruct ;

end;

registration

let c₃ be OrdTrapSpace;
cluster Lambda a₁ -> TrapSpace-like ;
correctness

proof end;

end;

definition

let c₃ be non empty AffinStruct ;
attr a₁ is Regular means :Def16: :: GEOMTRAP:def 16
for b₁, b₂, b₃, b₄, b₅, b₆, b₇, b₈, b₉, b₁₀ being Element of a₁ st b₁ <> b₂ & b₁,b₂ // b₃,b₄ & b₁,b₂ // b₅,b₆ & b₁,b₂ // b₇,b₈ & b₁,b₂ // b₉,b₁₀ & b₃,b₅ // b₇,b₉ holds
b₄,b₆ // b₈,b₁₀;

end;

:: deftheorem Def16 defines Regular GEOMTRAP:def 16 :

registration

cluster non empty strict Regular AffinStruct ;
existence

proof end;

end;

registration

let c₃ be MidOrdTrapSpace;
cluster Af a₁ -> non empty strict OrdTrapSpace-like Regular ;
correctness

proof end;

end;