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
canceled;
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 :
for n being Nat
for A being Subset of (REAL n) holds
( A is being_line iff ex x1, x2 being Element of REAL n st
( x1 <> x2 & A = Line (x1,x2) ) );
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
canceled;
theorem Th47:
theorem Th48:
theorem Th49:
:: deftheorem Def8 defines being_line EUCLID_4:def 8 :
for n being Nat
for A being Subset of (TOP-REAL n) holds
( A is being_line iff ex p1, p2 being Point of (TOP-REAL n) st
( p1 <> p2 & A = Line (p1,p2) ) );
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
theorem