begin
theorem Th1:
theorem Th2:
theorem Th3:
theorem
theorem
theorem
theorem
theorem
:: deftheorem defines Line EUCLID_4:def 1 :
for
n being
Nat for
x1,
x2 being
Element of
REAL n holds
Line x1,
x2 = { (((1 - lambda) * x1) + (lambda * x2)) where lambda is Real : verum } ;
Lm1:
for n being Nat
for x1, x2 being Element of REAL n holds Line x1,x2 c= Line x2,x1
theorem Th9:
theorem Th10:
Lm2:
for n being Nat
for x1, x2, x3 being Element of REAL n holds x1 + (x2 + x3) = (x1 + x2) + x3
by FINSEQOP:29;
theorem Th11:
theorem Th12:
:: deftheorem Def2 defines being_line EUCLID_4:def 2 :
Lm3:
for n being Nat
for A being Subset of (REAL n)
for x1, x2 being Element of REAL n st A is being_line & x1 in A & x2 in A & x1 <> x2 holds
A = Line x1,x2
theorem
theorem Th14:
theorem
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem Th21:
theorem Th22:
theorem Th23:
theorem
theorem Th25:
theorem Th26:
theorem
theorem Th28:
theorem
theorem
theorem Th31:
theorem
theorem
theorem
theorem Th35:
theorem Th36:
theorem Th37:
theorem Th38:
theorem
theorem
theorem
theorem
theorem
theorem
Lm4:
for a being Real
for n being Nat
for x being Element of REAL n holds
( - (a * x) = (- a) * x & - (a * x) = a * (- x) )
Lm5:
for n being Nat
for x1, x2 being Element of REAL n st x1 <> x2 holds
|.(x1 - x2).| <> 0
Lm6:
for n being Nat
for y1, y2, x1, x2 being Element of REAL n st y1 in Line x1,x2 & y2 in Line x1,x2 holds
ex a being Real st y1 - y2 = a * (x1 - x2)
Lm7:
for n being Nat
for x1, x2, y1 being Element of REAL n ex y2 being Element of REAL n st
( y2 in Line x1,x2 & x1 - x2,y1 - y2 are_orthogonal & ( for x being Element of REAL n st x in Line x1,x2 holds
|.(y1 - y2).| <= |.(y1 - x).| ) )
theorem
:: deftheorem EUCLID_4:def 3 :
canceled;
:: deftheorem EUCLID_4:def 4 :
canceled;
:: deftheorem EUCLID_4:def 5 :
canceled;
:: deftheorem EUCLID_4:def 6 :
canceled;
:: deftheorem defines Line EUCLID_4:def 7 :
for
n being
Nat for
p1,
p2 being
Point of
(TOP-REAL n) holds
Line p1,
p2 = { (((1 - lambda) * p1) + (lambda * p2)) where lambda is Real : verum } ;
Lm8:
for n being Nat
for p1, p2 being Point of (TOP-REAL n) ex x1, x2 being Element of REAL n st
( p1 = x1 & p2 = x2 & Line x1,x2 = Line p1,p2 )
theorem Th46:
theorem Th47:
theorem Th48:
theorem Th49:
:: deftheorem Def8 defines being_line EUCLID_4:def 8 :
Lm9:
for n being Nat
for A being Subset of (TOP-REAL n)
for p1, p2 being Point of (TOP-REAL n) st A is being_line & p1 in A & p2 in A & p1 <> p2 holds
A = Line p1,p2
theorem
theorem Th51:
theorem
:: deftheorem defines TPn2Rn EUCLID_4:def 9 :
theorem