:: Lines on Planes in $n$-Dimensional Euclidean Spaces
:: by Akihiro Kubo
::
:: Received May 24, 2005
:: Copyright (c) 2005-2021 Association of Mizar Users


:: Preliminaries
theorem Th1: :: EUCLIDLP:1
for s, t, u being Real
for n being Nat
for x being Element of REAL n holds
( (s / t) * (u * x) = ((s * u) / t) * x & (1 / t) * (u * x) = (u / t) * x )
proof end;

theorem Th2: :: EUCLIDLP:2
for n being Nat
for x being Element of REAL n holds
( x - x = 0* n & x + (- x) = 0* n )
proof end;

theorem Th3: :: EUCLIDLP:3
for a being Real
for n being Nat
for x being Element of REAL n holds
( - (a * x) = (- a) * x & - (a * x) = a * (- x) )
proof end;

theorem Th4: :: EUCLIDLP:4
for n being Nat
for x1, x2, x3 being Element of REAL n holds x1 - (x2 - x3) = (x1 - x2) + x3
proof end;

theorem Th5: :: EUCLIDLP:5
for n being Nat
for x1, x2, x3 being Element of REAL n holds x1 + (x2 - x3) = (x1 + x2) - x3
proof end;

theorem Th6: :: EUCLIDLP:6
for n being Nat
for x1, x2, x3 being Element of REAL n holds
( x1 = x2 + x3 iff x2 = x1 - x3 )
proof end;

theorem Th7: :: EUCLIDLP:7
for n being Nat
for x, x1, x2, x3 being Element of REAL n holds
( x = (x1 + x2) + x3 iff x - x1 = x2 + x3 )
proof end;

theorem Th8: :: EUCLIDLP:8
for n being Nat
for x1, x2, x3 being Element of REAL n holds - ((x1 + x2) + x3) = ((- x1) + (- x2)) + (- x3)
proof end;

Lm1: for n being Nat
for x1, x2 being Element of REAL n st x1 <> x2 holds
|.(x1 - x2).| <> 0
proof end;

theorem Th9: :: EUCLIDLP:9
for n being Nat
for x1, x2 being Element of REAL n holds
( x1 = x2 iff x1 - x2 = 0* n )
proof end;

theorem Th10: :: EUCLIDLP:10
for t being Real
for n being Nat
for x0, x, x1 being Element of REAL n st x1 - x0 = t * x & x1 <> x0 holds
t <> 0
proof end;

theorem Th11: :: EUCLIDLP:11
for a, b being Real
for n being Nat
for x being Element of REAL n holds
( (a - b) * x = (a * x) + ((- b) * x) & (a - b) * x = (a * x) + (- (b * x)) & (a - b) * x = (a * x) - (b * x) )
proof end;

theorem Th12: :: EUCLIDLP:12
for a being Real
for n being Nat
for x, y being Element of REAL n holds
( a * (x - y) = (a * x) + (- (a * y)) & a * (x - y) = (a * x) + ((- a) * y) & a * (x - y) = (a * x) - (a * y) )
proof end;

theorem Th13: :: EUCLIDLP:13
for s, t, u being Real
for n being Nat
for x being Element of REAL n holds ((s - t) - u) * x = ((s * x) - (t * x)) - (u * x)
proof end;

theorem Th14: :: EUCLIDLP:14
for a1, a2, a3 being Real
for n being Nat
for x, x1, x2, x3 being Element of REAL n holds x - (((a1 * x1) + (a2 * x2)) + (a3 * x3)) = x + ((((- a1) * x1) + ((- a2) * x2)) + ((- a3) * x3))
proof end;

theorem :: EUCLIDLP:15
for s, t, u being Real
for n being Nat
for x, y being Element of REAL n holds x - (((s + t) + u) * y) = ((x + ((- s) * y)) + ((- t) * y)) + ((- u) * y)
proof end;

theorem Th16: :: EUCLIDLP:16
for n being Nat
for x1, x2, y1, y2 being Element of REAL n holds (x1 + x2) + (y1 + y2) = (x1 + y1) + (x2 + y2)
proof end;

theorem Th17: :: EUCLIDLP:17
for n being Nat
for x1, x2, x3, y1, y2, y3 being Element of REAL n holds ((x1 + x2) + x3) + ((y1 + y2) + y3) = ((x1 + y1) + (x2 + y2)) + (x3 + y3)
proof end;

theorem Th18: :: EUCLIDLP:18
for n being Nat
for x1, x2, y1, y2 being Element of REAL n holds (x1 + x2) - (y1 + y2) = (x1 - y1) + (x2 - y2)
proof end;

theorem :: EUCLIDLP:19
for n being Nat
for x1, x2, x3, y1, y2, y3 being Element of REAL n holds ((x1 + x2) + x3) - ((y1 + y2) + y3) = ((x1 - y1) + (x2 - y2)) + (x3 - y3)
proof end;

theorem Th20: :: EUCLIDLP:20
for a being Real
for n being Nat
for x1, x2, x3 being Element of REAL n holds a * ((x1 + x2) + x3) = ((a * x1) + (a * x2)) + (a * x3)
proof end;

theorem Th21: :: EUCLIDLP:21
for a, b1, b2 being Real
for n being Nat
for x1, x2 being Element of REAL n holds a * ((b1 * x1) + (b2 * x2)) = ((a * b1) * x1) + ((a * b2) * x2)
proof end;

theorem Th22: :: EUCLIDLP:22
for a, b1, b2, b3 being Real
for n being Nat
for x1, x2, x3 being Element of REAL n holds a * (((b1 * x1) + (b2 * x2)) + (b3 * x3)) = (((a * b1) * x1) + ((a * b2) * x2)) + ((a * b3) * x3)
proof end;

theorem Th23: :: EUCLIDLP:23
for a1, a2, b1, b2 being Real
for n being Nat
for x1, x2 being Element of REAL n holds ((a1 * x1) + (a2 * x2)) + ((b1 * x1) + (b2 * x2)) = ((a1 + b1) * x1) + ((a2 + b2) * x2)
proof end;

theorem Th24: :: EUCLIDLP:24
for a1, a2, a3, b1, b2, b3 being Real
for n being Nat
for x1, x2, x3 being Element of REAL n holds (((a1 * x1) + (a2 * x2)) + (a3 * x3)) + (((b1 * x1) + (b2 * x2)) + (b3 * x3)) = (((a1 + b1) * x1) + ((a2 + b2) * x2)) + ((a3 + b3) * x3)
proof end;

theorem Th25: :: EUCLIDLP:25
for a1, a2, b1, b2 being Real
for n being Nat
for x1, x2 being Element of REAL n holds ((a1 * x1) + (a2 * x2)) - ((b1 * x1) + (b2 * x2)) = ((a1 - b1) * x1) + ((a2 - b2) * x2)
proof end;

theorem Th26: :: EUCLIDLP:26
for a1, a2, a3, b1, b2, b3 being Real
for n being Nat
for x1, x2, x3 being Element of REAL n holds (((a1 * x1) + (a2 * x2)) + (a3 * x3)) - (((b1 * x1) + (b2 * x2)) + (b3 * x3)) = (((a1 - b1) * x1) + ((a2 - b2) * x2)) + ((a3 - b3) * x3)
proof end;

theorem Th27: :: EUCLIDLP:27
for a1, a2, a3 being Real
for n being Nat
for x1, x2, x3 being Element of REAL n st (a1 + a2) + a3 = 1 holds
((a1 * x1) + (a2 * x2)) + (a3 * x3) = (x1 + (a2 * (x2 - x1))) + (a3 * (x3 - x1))
proof end;

theorem Th28: :: EUCLIDLP:28
for a2, a3 being Real
for n being Nat
for x, x1, x2, x3 being Element of REAL n st x = (x1 + (a2 * (x2 - x1))) + (a3 * (x3 - x1)) holds
ex a1 being Real st
( x = ((a1 * x1) + (a2 * x2)) + (a3 * x3) & (a1 + a2) + a3 = 1 )
proof end;

theorem :: EUCLIDLP:29
for n being Nat st n >= 1 holds
1* n <> 0* n
proof end;

:: Lines
theorem Th30: :: EUCLIDLP:30
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)
proof end;

theorem Th31: :: EUCLIDLP:31
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 y2 - y1 = a * (x2 - x1)
proof end;

definition
let n be Nat;
let x1, x2 be Element of REAL n;
pred x1 // x2 means :Def1: :: EUCLIDLP:def 1
( x1 <> 0* n & x2 <> 0* n & ex r being Real st x1 = r * x2 );
end;

:: deftheorem Def1 defines // EUCLIDLP:def 1 :
for n being Nat
for x1, x2 being Element of REAL n holds
( x1 // x2 iff ( x1 <> 0* n & x2 <> 0* n & ex r being Real st x1 = r * x2 ) );

theorem Th32: :: EUCLIDLP:32
for n being Nat
for x1, x2 being Element of REAL n st x1 // x2 holds
ex a being Real st
( a <> 0 & x1 = a * x2 )
proof end;

definition
let n be Nat;
let x1, x2 be Element of REAL n;
:: original: //
redefine pred x1 // x2;
symmetry
for x1, x2 being Element of REAL n st (n,b1,b2) holds
(n,b2,b1)
proof end;
end;

theorem Th33: :: EUCLIDLP:33
for n being Nat
for x1, x2, x3 being Element of REAL n st x1 // x2 & x2 // x3 holds
x1 // x3
proof end;

definition
let n be Nat;
let x1, x2 be Element of REAL n;
pred x1,x2 are_lindependent2 means :: EUCLIDLP:def 2
 for a1, a2 being Real st (a1 * x1) + (a2 * x2) = 0* n holds
( a1 = 0 & a2 = 0 );
symmetry
for x1, x2 being Element of REAL n st ( for a1, a2 being Real st (a1 * x1) + (a2 * x2) = 0* n holds
( a1 = 0 & a2 = 0 ) ) holds
for a1, a2 being Real st (a1 * x2) + (a2 * x1) = 0* n holds
( a1 = 0 & a2 = 0 ) ;
end;

:: deftheorem defines are_lindependent2 EUCLIDLP:def 2 :
for n being Nat
for x1, x2 being Element of REAL n holds
( x1,x2 are_lindependent2 iff for a1, a2 being Real st (a1 * x1) + (a2 * x2) = 0* n holds
( a1 = 0 & a2 = 0 ) );

notation
let n be Nat;
let x1, x2 be Element of REAL n;
antonym x1,x2 are_ldependent2 for x1,x2 are_lindependent2 ;
end;

Lm2: for n being Nat
for x1, x2 being Element of REAL n st x1,x2 are_lindependent2 holds
x1 <> 0* n
proof end;

theorem :: EUCLIDLP:34
for n being Nat
for x1, x2 being Element of REAL n st x1,x2 are_lindependent2 holds
( x1 <> 0* n & x2 <> 0* n ) by Lm2;

theorem Th35: :: EUCLIDLP:35
for a1, a2, b1, b2 being Real
for n being Nat
for x1, x2 being Element of REAL n st x1,x2 are_lindependent2 & (a1 * x1) + (a2 * x2) = (b1 * x1) + (b2 * x2) holds
( a1 = b1 & a2 = b2 )
proof end;

theorem Th36: :: EUCLIDLP:36
for a1, a2, b1, b2 being Real
for n being Nat
for y2, x1, x2, y1, y1 being Element of REAL n st y1,y2 are_lindependent2 & y1 = (a1 * x1) + (a2 * x2) & y2 = (b1 * x1) + (b2 * x2) holds
ex c1, c2, d1, d2 being Real st
( x1 = (c1 * y1) + (c2 * y2) & x2 = (d1 * y1) + (d2 * y2) )
proof end;

theorem Th37: :: EUCLIDLP:37
for n being Nat
for x1, x2 being Element of REAL n st x1,x2 are_lindependent2 holds
x1 <> x2
proof end;

theorem :: EUCLIDLP:38
for n being Nat
for x1, x2, x3 being Element of REAL n st x2 - x1,x3 - x1 are_lindependent2 holds
x2 <> x3 by Th37;

theorem :: EUCLIDLP:39
for t being Real
for n being Nat
for x1, x2 being Element of REAL n st x1,x2 are_lindependent2 holds
x1 + (t * x2),x2 are_lindependent2
proof end;

theorem Th40: :: EUCLIDLP:40
for n being Nat
for x0, x1, x2, x3, y0, y1, y2, y3 being Element of REAL n st x1 - x0,x3 - x2 are_lindependent2 & y0 in Line (x0,x1) & y1 in Line (x0,x1) & y0 <> y1 & y2 in Line (x2,x3) & y3 in Line (x2,x3) & y2 <> y3 holds
y1 - y0,y3 - y2 are_lindependent2
proof end;

Lm3: for n being Nat
for x1, x2 being Element of REAL n st x1 // x2 holds
x1,x2 are_ldependent2
proof end;

theorem :: EUCLIDLP:41
for n being Nat
for x1, x2 being Element of REAL n st x1 // x2 holds
( x1,x2 are_ldependent2 & x1 <> 0* n & x2 <> 0* n ) by Lm3;

Lm4: for n being Nat
for x1, x2 being Element of REAL n st x1,x2 are_ldependent2 & x1 <> 0* n & x2 <> 0* n holds
x1 // x2
proof end;

theorem :: EUCLIDLP:42
for n being Nat
for x1, x2 being Element of REAL n holds
( not x1,x2 are_ldependent2 or x1 = 0* n or x2 = 0* n or x1 // x2 ) by Lm4;

theorem Th43: :: EUCLIDLP:43
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 )
proof end;

definition
let n be Nat;
let x1, x2 be Element of REAL n;
pred x1 _|_ x2 means :: EUCLIDLP:def 3
( x1 <> 0* n & x2 <> 0* n & x1,x2 are_orthogonal );
symmetry
for x1, x2 being Element of REAL n st x1 <> 0* n & x2 <> 0* n & x1,x2 are_orthogonal holds
( x2 <> 0* n & x1 <> 0* n & x2,x1 are_orthogonal ) ;
end;

:: deftheorem defines _|_ EUCLIDLP:def 3 :
for n being Nat
for x1, x2 being Element of REAL n holds
( x1 _|_ x2 iff ( x1 <> 0* n & x2 <> 0* n & x1,x2 are_orthogonal ) );

theorem Th44: :: EUCLIDLP:44
for n being Nat
for x, y0, y1 being Element of REAL n st x _|_ y0 & y0 // y1 holds
x _|_ y1
proof end;

theorem Th45: :: EUCLIDLP:45
for n being Nat
for x, y being Element of REAL n st x _|_ y holds
x,y are_lindependent2
proof end;

theorem :: EUCLIDLP:46
for n being Nat
for x1, x2 being Element of REAL n st x1 // x2 holds
not x1 _|_ x2
proof end;

definition
let n be Nat;
func line_of_REAL n -> Subset-Family of (REAL n) equals :: EUCLIDLP:def 4
 { (Line (x1,x2)) where x1, x2 is Element of REAL n : verum } ;
correctness
coherence
{ (Line (x1,x2)) where x1, x2 is Element of REAL n : verum } is Subset-Family of (REAL n);
proof end;
end;

:: deftheorem defines line_of_REAL EUCLIDLP:def 4 :
for n being Nat holds line_of_REAL n = { (Line (x1,x2)) where x1, x2 is Element of REAL n : verum } ;

registration
let n be Nat;
cluster line_of_REAL n -> non empty ;
coherence
not line_of_REAL n is empty
proof end;
end;

theorem Th47: :: EUCLIDLP:47
for n being Nat
for x1, x2 being Element of REAL n holds Line (x1,x2) in line_of_REAL n ;

theorem Th48: :: EUCLIDLP:48
for n being Nat
for x1, x2 being Element of REAL n
for L being Element of line_of_REAL n st x1 in L & x2 in L holds
Line (x1,x2) c= L
proof end;

theorem Th49: :: EUCLIDLP:49
for n being Nat
for L1, L2 being Element of line_of_REAL n holds
( L1 meets L2 iff ex x being Element of REAL n st
( x in L1 & x in L2 ) )
proof end;

theorem :: EUCLIDLP:50
for n being Nat
for x being Element of REAL n
for L0, L1 being Element of line_of_REAL n st L0 misses L1 & x in L0 holds
not x in L1 by Th49;

theorem Th51: :: EUCLIDLP:51
for n being Nat
for L being Element of line_of_REAL n ex x1, x2 being Element of REAL n st L = Line (x1,x2)
proof end;

theorem Th52: :: EUCLIDLP:52
for n being Nat
for L being Element of line_of_REAL n ex x being Element of REAL n st x in L
proof end;

theorem Th53: :: EUCLIDLP:53
for n being Nat
for x0 being Element of REAL n
for L being Element of line_of_REAL n st L is being_line holds
ex x1 being Element of REAL n st
( x1 <> x0 & x1 in L )
proof end;

theorem Th54: :: EUCLIDLP:54
for n being Nat
for x being Element of REAL n
for L being Element of line_of_REAL n st not x in L & L is being_line holds
ex x1, x2 being Element of REAL n st
( L = Line (x1,x2) & x - x1 _|_ x2 - x1 )
proof end;

theorem Th55: :: EUCLIDLP:55
for n being Nat
for x being Element of REAL n
for L being Element of line_of_REAL n st not x in L & L is being_line holds
ex x1, x2 being Element of REAL n st
( L = Line (x1,x2) & x - x1,x2 - x1 are_lindependent2 )
proof end;

definition
let n be Nat;
let x be Element of REAL n;
let L be Element of line_of_REAL n;
func dist_v (x,L) -> Subset of REAL equals :: EUCLIDLP:def 5
 { |.(x - x0).| where x0 is Element of REAL n : x0 in L } ;
correctness
coherence
{ |.(x - x0).| where x0 is Element of REAL n : x0 in L } is Subset of REAL;
proof end;
end;

:: deftheorem defines dist_v EUCLIDLP:def 5 :
for n being Nat
for x being Element of REAL n
for L being Element of line_of_REAL n holds dist_v (x,L) = { |.(x - x0).| where x0 is Element of REAL n : x0 in L } ;

definition
let n be Nat;
let x be Element of REAL n;
let L be Element of line_of_REAL n;
func dist (x,L) -> Real equals :: EUCLIDLP:def 6
 lower_bound (dist_v (x,L));
correctness
coherence
lower_bound (dist_v (x,L)) is Real;
;
end;

:: deftheorem defines dist EUCLIDLP:def 6 :
for n being Nat
for x being Element of REAL n
for L being Element of line_of_REAL n holds dist (x,L) = lower_bound (dist_v (x,L));

theorem :: EUCLIDLP:56
for n being Nat
for x, x1, x2 being Element of REAL n
for L being Element of line_of_REAL n st L = Line (x1,x2) holds
{ |.(x - x0).| where x0 is Element of REAL n : x0 in Line (x1,x2) } = dist_v (x,L) ;

theorem Th57: :: EUCLIDLP:57
for n being Nat
for x being Element of REAL n
for L being Element of line_of_REAL n ex x0 being Element of REAL n st
( x0 in L & |.(x - x0).| = dist (x,L) )
proof end;

theorem :: EUCLIDLP:58
for n being Nat
for x being Element of REAL n
for L being Element of line_of_REAL n holds dist (x,L) >= 0
proof end;

theorem :: EUCLIDLP:59
for n being Nat
for x being Element of REAL n
for L being Element of line_of_REAL n holds
( x in L iff dist (x,L) = 0 )
proof end;

definition
let n be Nat;
let L1, L2 be Element of line_of_REAL n;
pred L1 // L2 means :: EUCLIDLP:def 7
 ex x1, x2, y1, y2 being Element of REAL n st
( L1 = Line (x1,x2) & L2 = Line (y1,y2) & x2 - x1 // y2 - y1 );
symmetry
for L1, L2 being Element of line_of_REAL n st ex x1, x2, y1, y2 being Element of REAL n st
( L1 = Line (x1,x2) & L2 = Line (y1,y2) & x2 - x1 // y2 - y1 ) holds
ex x1, x2, y1, y2 being Element of REAL n st
( L2 = Line (x1,x2) & L1 = Line (y1,y2) & x2 - x1 // y2 - y1 ) ;
end;

:: deftheorem defines // EUCLIDLP:def 7 :
for n being Nat
for L1, L2 being Element of line_of_REAL n holds
( L1 // L2 iff ex x1, x2, y1, y2 being Element of REAL n st
( L1 = Line (x1,x2) & L2 = Line (y1,y2) & x2 - x1 // y2 - y1 ) );

theorem :: EUCLIDLP:60
for n being Nat
for L0, L1, L2 being Element of line_of_REAL n st L0 // L1 & L1 // L2 holds
L0 // L2
proof end;

definition
let n be Nat;
let L1, L2 be Element of line_of_REAL n;
pred L1 _|_ L2 means :: EUCLIDLP:def 8
 ex x1, x2, y1, y2 being Element of REAL n st
( L1 = Line (x1,x2) & L2 = Line (y1,y2) & x2 - x1 _|_ y2 - y1 );
symmetry
for L1, L2 being Element of line_of_REAL n st ex x1, x2, y1, y2 being Element of REAL n st
( L1 = Line (x1,x2) & L2 = Line (y1,y2) & x2 - x1 _|_ y2 - y1 ) holds
ex x1, x2, y1, y2 being Element of REAL n st
( L2 = Line (x1,x2) & L1 = Line (y1,y2) & x2 - x1 _|_ y2 - y1 ) ;
end;

:: deftheorem defines _|_ EUCLIDLP:def 8 :
for n being Nat
for L1, L2 being Element of line_of_REAL n holds
( L1 _|_ L2 iff ex x1, x2, y1, y2 being Element of REAL n st
( L1 = Line (x1,x2) & L2 = Line (y1,y2) & x2 - x1 _|_ y2 - y1 ) );

theorem Th61: :: EUCLIDLP:61
for n being Nat
for L0, L1, L2 being Element of line_of_REAL n st L0 _|_ L1 & L1 // L2 holds
L0 _|_ L2
proof end;

theorem Th62: :: EUCLIDLP:62
for n being Nat
for x being Element of REAL n
for L being Element of line_of_REAL n st not x in L & L is being_line holds
ex L0 being Element of line_of_REAL n st
( x in L0 & L0 _|_ L & L0 meets L )
proof end;

theorem Th63: :: EUCLIDLP:63
for n being Nat
for L1, L2 being Element of line_of_REAL n st L1 misses L2 holds
ex x being Element of REAL n st
( x in L1 & not x in L2 )
proof end;

theorem Th64: :: EUCLIDLP:64
for n being Nat
for x1, x2 being Element of REAL n
for L being Element of line_of_REAL n st x1 in L & x2 in L & x1 <> x2 holds
( Line (x1,x2) = L & L is being_line )
proof end;

theorem Th65: :: EUCLIDLP:65
for n being Nat
for L1, L2 being Element of line_of_REAL n st L1 is being_line & L1 = L2 holds
L1 // L2
proof end;

theorem Th66: :: EUCLIDLP:66
for n being Nat
for L1, L2 being Element of line_of_REAL n st L1 // L2 holds
( L1 is being_line & L2 is being_line )
proof end;

theorem Th67: :: EUCLIDLP:67
for n being Nat
for L1, L2 being Element of line_of_REAL n st L1 _|_ L2 holds
( L1 is being_line & L2 is being_line )
proof end;

theorem :: EUCLIDLP:68
for a being Real
for n being Nat
for x being Element of REAL n
for L being Element of line_of_REAL n st x in L & a <> 1 & a * x in L holds
0* n in L
proof end;

theorem :: EUCLIDLP:69
for a being Real
for n being Nat
for x1, x2 being Element of REAL n
for L being Element of line_of_REAL n st x1 in L & x2 in L holds
ex x3 being Element of REAL n st
( x3 in L & x3 - x1 = a * (x2 - x1) )
proof end;

theorem Th70: :: EUCLIDLP:70
for n being Nat
for x1, x2, x3 being Element of REAL n
for L being Element of line_of_REAL n st x1 in L & x2 in L & x3 in L & x1 <> x2 holds
ex a being Real st x3 - x1 = a * (x2 - x1)
proof end;

theorem Th71: :: EUCLIDLP:71
for n being Nat
for L1, L2 being Element of line_of_REAL n st L1 // L2 & L1 <> L2 holds
L1 misses L2
proof end;

theorem Th72: :: EUCLIDLP:72
for n being Nat
for x being Element of REAL n
for L being Element of line_of_REAL n st L is being_line holds
ex L0 being Element of line_of_REAL n st
( x in L0 & L0 // L )
proof end;

theorem :: EUCLIDLP:73
for n being Nat
for x being Element of REAL n
for L being Element of line_of_REAL n st not x in L & L is being_line holds
ex L0 being Element of line_of_REAL n st
( x in L0 & L0 // L & L0 <> L )
proof end;

theorem Th74: :: EUCLIDLP:74
for n being Nat
for x0, x1, y0, y1 being Element of REAL n
for L1, L2 being Element of line_of_REAL n st x0 in L1 & x1 in L1 & x0 <> x1 & y0 in L2 & y1 in L2 & y0 <> y1 & L1 _|_ L2 holds
x1 - x0 _|_ y1 - y0
proof end;

theorem Th75: :: EUCLIDLP:75
for n being Nat
for L1, L2 being Element of line_of_REAL n st L1 _|_ L2 holds
L1 <> L2
proof end;

theorem Th76: :: EUCLIDLP:76
for n being Nat
for x1, x2 being Element of REAL n
for L being Element of line_of_REAL n st L is being_line & L = Line (x1,x2) holds
x1 <> x2
proof end;

theorem Th77: :: EUCLIDLP:77
for n being Nat
for x0, x1, y0, y1 being Element of REAL n
for L1, L2 being Element of line_of_REAL n st x0 in L1 & x1 in L1 & x0 <> x1 & y0 in L2 & y1 in L2 & y0 <> y1 & L1 // L2 holds
x1 - x0 // y1 - y0
proof end;

theorem :: EUCLIDLP:78
for n being Nat
for x1, x2, x3, y2, y3 being Element of REAL n
for L1, L2 being Element of line_of_REAL n st x2 - x1,x3 - x1 are_lindependent2 & y2 in Line (x1,x2) & y3 in Line (x1,x3) & L1 = Line (x2,x3) & L2 = Line (y2,y3) holds
( L1 // L2 iff ex a being Real st
( a <> 0 & y2 - x1 = a * (x2 - x1) & y3 - x1 = a * (x3 - x1) ) )
proof end;

theorem Th79: :: EUCLIDLP:79
for n being Nat
for L1, L2 being Element of line_of_REAL n st L1 is being_line & L2 is being_line & L1 <> L2 holds
ex x being Element of REAL n st
( x in L1 & not x in L2 )
proof end;

theorem Th80: :: EUCLIDLP:80
for n being Nat
for x being Element of REAL n
for L1, L2 being Element of line_of_REAL n st L1 _|_ L2 holds
ex L0 being Element of line_of_REAL n st
( x in L0 & L0 _|_ L2 & L0 // L1 )
proof end;

theorem Th81: :: EUCLIDLP:81
for n being Nat
for x being Element of REAL n
for L1, L2 being Element of line_of_REAL n st x in L2 & L1 _|_ L2 holds
ex x0 being Element of REAL n st
( x <> x0 & x0 in L1 & not x0 in L2 )
proof end;

:: Planes
definition
let n be Nat;
let x1, x2, x3 be Element of REAL n;
func plane (x1,x2,x3) -> Subset of (REAL n) equals :: EUCLIDLP:def 9
 { x where x is Element of REAL n : ex a1, a2, a3 being Real st
( (a1 + a2) + a3 = 1 & x = ((a1 * x1) + (a2 * x2)) + (a3 * x3) ) } ;
correctness
coherence
{ x where x is Element of REAL n : ex a1, a2, a3 being Real st
( (a1 + a2) + a3 = 1 & x = ((a1 * x1) + (a2 * x2)) + (a3 * x3) ) } is Subset of (REAL n);
proof end;
end;

:: deftheorem defines plane EUCLIDLP:def 9 :
for n being Nat
for x1, x2, x3 being Element of REAL n holds plane (x1,x2,x3) = { x where x is Element of REAL n : ex a1, a2, a3 being Real st
( (a1 + a2) + a3 = 1 & x = ((a1 * x1) + (a2 * x2)) + (a3 * x3) ) } ;

registration
let n be Nat;
let x1, x2, x3 be Element of REAL n;
cluster plane (x1,x2,x3) -> non empty ;
coherence
not plane (x1,x2,x3) is empty
proof end;
end;

definition
let n be Nat;
let A be Subset of (REAL n);
attr A is being_plane means :: EUCLIDLP:def 10
 ex x1, x2, x3 being Element of REAL n st
( x2 - x1,x3 - x1 are_lindependent2 & A = plane (x1,x2,x3) );
end;

:: deftheorem defines being_plane EUCLIDLP:def 10 :
for n being Nat
for A being Subset of (REAL n) holds
( A is being_plane iff ex x1, x2, x3 being Element of REAL n st
( x2 - x1,x3 - x1 are_lindependent2 & A = plane (x1,x2,x3) ) );

theorem Th82: :: EUCLIDLP:82
for n being Nat
for x1, x2, x3 being Element of REAL n holds
( x1 in plane (x1,x2,x3) & x2 in plane (x1,x2,x3) & x3 in plane (x1,x2,x3) )
proof end;

theorem Th83: :: EUCLIDLP:83
for n being Nat
for x1, x2, x3, y1, y2, y3 being Element of REAL n st x1 in plane (y1,y2,y3) & x2 in plane (y1,y2,y3) & x3 in plane (y1,y2,y3) holds
plane (x1,x2,x3) c= plane (y1,y2,y3)
proof end;

theorem :: EUCLIDLP:84
for n being Nat
for A being Subset of (REAL n)
for x, x1, x2, x3 being Element of REAL n st x in plane (x1,x2,x3) & ex c1, c2, c3 being Real st
( (c1 + c2) + c3 = 0 & x = ((c1 * x1) + (c2 * x2)) + (c3 * x3) ) holds
0* n in plane (x1,x2,x3)
proof end;

theorem Th85: :: EUCLIDLP:85
for n being Nat
for x1, x2, x3, y1, y2 being Element of REAL n st y1 in plane (x1,x2,x3) & y2 in plane (x1,x2,x3) holds
Line (y1,y2) c= plane (x1,x2,x3)
proof end;

theorem :: EUCLIDLP:86
for n being Nat
for A being Subset of (REAL n)
for x being Element of REAL n st A is being_plane & x in A & ex a being Real st
( a <> 1 & a * x in A ) holds
0* n in A
proof end;

theorem :: EUCLIDLP:87
for a1, a2, a3 being Real
for n being Nat
for x, x1, x2, x3 being Element of REAL n st x in plane (x1,x2,x3) & x = ((a1 * x1) + (a2 * x2)) + (a3 * x3) & not (a1 + a2) + a3 = 1 holds
0* n in plane (x1,x2,x3)
proof end;

theorem Th88: :: EUCLIDLP:88
for n being Nat
for x, x1, x2, x3 being Element of REAL n holds
( x in plane (x1,x2,x3) iff ex a1, a2, a3 being Real st
( (a1 + a2) + a3 = 1 & x = ((a1 * x1) + (a2 * x2)) + (a3 * x3) ) )
proof end;

theorem :: EUCLIDLP:89
for a1, a2, a3, b1, b2, b3 being Real
for n being Nat
for x, x1, x2, x3 being Element of REAL n st x2 - x1,x3 - x1 are_lindependent2 & (a1 + a2) + a3 = 1 & x = ((a1 * x1) + (a2 * x2)) + (a3 * x3) & (b1 + b2) + b3 = 1 & x = ((b1 * x1) + (b2 * x2)) + (b3 * x3) holds
( a1 = b1 & a2 = b2 & a3 = b3 )
proof end;

definition
let n be Nat;
func plane_of_REAL n -> Subset-Family of (REAL n) equals :: EUCLIDLP:def 11
 { P where P is Subset of (REAL n) : ex x1, x2, x3 being Element of REAL n st P = plane (x1,x2,x3) } ;
correctness
coherence
{ P where P is Subset of (REAL n) : ex x1, x2, x3 being Element of REAL n st P = plane (x1,x2,x3) } is Subset-Family of (REAL n);
proof end;
end;

:: deftheorem defines plane_of_REAL EUCLIDLP:def 11 :
for n being Nat holds plane_of_REAL n = { P where P is Subset of (REAL n) : ex x1, x2, x3 being Element of REAL n st P = plane (x1,x2,x3) } ;

registration
let n be Nat;
cluster plane_of_REAL n -> non empty ;
coherence
not plane_of_REAL n is empty
proof end;
end;

theorem Th90: :: EUCLIDLP:90
for n being Nat
for x1, x2, x3 being Element of REAL n holds plane (x1,x2,x3) in plane_of_REAL n ;

theorem Th91: :: EUCLIDLP:91
for n being Nat
for x1, x2, x3 being Element of REAL n
for P being Element of plane_of_REAL n st x1 in P & x2 in P & x3 in P holds
plane (x1,x2,x3) c= P
proof end;

theorem Th92: :: EUCLIDLP:92
for n being Nat
for x1, x2, x3 being Element of REAL n
for P being Element of plane_of_REAL n st x1 in P & x2 in P & x3 in P & x2 - x1,x3 - x1 are_lindependent2 holds
P = plane (x1,x2,x3)
proof end;

theorem :: EUCLIDLP:93
for n being Nat
for P1, P2 being Element of plane_of_REAL n st P1 is being_plane & P1 c= P2 holds
P1 = P2
proof end;

:: Lines in the planes
theorem :: EUCLIDLP:94
for n being Nat
for x1, x2, x3 being Element of REAL n holds
( Line (x1,x2) c= plane (x1,x2,x3) & Line (x2,x3) c= plane (x1,x2,x3) & Line (x3,x1) c= plane (x1,x2,x3) )
proof end;

theorem Th95: :: EUCLIDLP:95
for n being Nat
for x1, x2 being Element of REAL n
for P being Element of plane_of_REAL n st x1 in P & x2 in P holds
Line (x1,x2) c= P
proof end;

definition
let n be Nat;
let L1, L2 be Element of line_of_REAL n;
pred L1,L2 are_coplane means :: EUCLIDLP:def 12
 ex x1, x2, x3 being Element of REAL n st
( L1 c= plane (x1,x2,x3) & L2 c= plane (x1,x2,x3) );
end;

:: deftheorem defines are_coplane EUCLIDLP:def 12 :
for n being Nat
for L1, L2 being Element of line_of_REAL n holds
( L1,L2 are_coplane iff ex x1, x2, x3 being Element of REAL n st
( L1 c= plane (x1,x2,x3) & L2 c= plane (x1,x2,x3) ) );

theorem Th96: :: EUCLIDLP:96
for n being Nat
for L1, L2 being Element of line_of_REAL n holds
( L1,L2 are_coplane iff ex P being Element of plane_of_REAL n st
( L1 c= P & L2 c= P ) )
proof end;

theorem Th97: :: EUCLIDLP:97
for n being Nat
for L1, L2 being Element of line_of_REAL n st L1 // L2 holds
L1,L2 are_coplane
proof end;

theorem Th98: :: EUCLIDLP:98
for n being Nat
for L1, L2 being Element of line_of_REAL n st L1 is being_line & L2 is being_line & L1,L2 are_coplane & L1 misses L2 holds
ex P being Element of plane_of_REAL n st
( L1 c= P & L2 c= P & P is being_plane )
proof end;

theorem Th99: :: EUCLIDLP:99
for n being Nat
for x being Element of REAL n
for L being Element of line_of_REAL n ex P being Element of plane_of_REAL n st
( x in P & L c= P )
proof end;

theorem Th100: :: EUCLIDLP:100
for n being Nat
for x being Element of REAL n
for L being Element of line_of_REAL n st not x in L & L is being_line holds
ex P being Element of plane_of_REAL n st
( x in P & L c= P & P is being_plane )
proof end;

theorem Th101: :: EUCLIDLP:101
for n being Nat
for x being Element of REAL n
for L being Element of line_of_REAL n
for P being Element of plane_of_REAL n st x in P & L c= P & not x in L & L is being_line holds
P is being_plane
proof end;

theorem Th102: :: EUCLIDLP:102
for n being Nat
for x being Element of REAL n
for L being Element of line_of_REAL n
for P0, P1 being Element of plane_of_REAL n st not x in L & L is being_line & x in P0 & L c= P0 & x in P1 & L c= P1 holds
P0 = P1
proof end;

theorem :: EUCLIDLP:103
for n being Nat
for L1, L2 being Element of line_of_REAL n st L1 is being_line & L2 is being_line & L1,L2 are_coplane & L1 <> L2 holds
ex P being Element of plane_of_REAL n st
( L1 c= P & L2 c= P & P is being_plane )
proof end;

theorem :: EUCLIDLP:104
for n being Nat
for L1, L2 being Element of line_of_REAL n st L1 is being_line & L2 is being_line & L1 <> L2 & L1 meets L2 holds
ex P being Element of plane_of_REAL n st
( L1 c= P & L2 c= P & P is being_plane )
proof end;

theorem :: EUCLIDLP:105
for n being Nat
for L1, L2 being Element of line_of_REAL n
for P1, P2 being Element of plane_of_REAL n st L1 is being_line & L2 is being_line & L1 <> L2 & L1 c= P1 & L2 c= P1 & L1 c= P2 & L2 c= P2 holds
P1 = P2
proof end;

theorem Th106: :: EUCLIDLP:106
for n being Nat
for L1, L2 being Element of line_of_REAL n st L1 // L2 & L1 <> L2 holds
ex P being Element of plane_of_REAL n st
( L1 c= P & L2 c= P & P is being_plane )
proof end;

theorem Th107: :: EUCLIDLP:107
for n being Nat
for L1, L2 being Element of line_of_REAL n st L1 _|_ L2 & L1 meets L2 holds
ex P being Element of plane_of_REAL n st
( P is being_plane & L1 c= P & L2 c= P )
proof end;

theorem Th108: :: EUCLIDLP:108
for n being Nat
for x being Element of REAL n
for L0, L1, L2 being Element of line_of_REAL n
for P being Element of plane_of_REAL n st L0 c= P & L1 c= P & L2 c= P & x in L0 & x in L1 & x in L2 & L0 _|_ L2 & L1 _|_ L2 holds
L0 = L1
proof end;

theorem Th109: :: EUCLIDLP:109
for n being Nat
for L1, L2 being Element of line_of_REAL n st L1,L2 are_coplane & L1 _|_ L2 holds
L1 meets L2
proof end;

theorem Th110: :: EUCLIDLP:110
for n being Nat
for x being Element of REAL n
for L0, L1, L2 being Element of line_of_REAL n
for P being Element of plane_of_REAL n st L1 c= P & L2 c= P & L1 _|_ L2 & x in P & L0 // L2 & x in L0 holds
( L0 c= P & L0 _|_ L1 )
proof end;

theorem Th111: :: EUCLIDLP:111
for n being Nat
for L, L1, L2 being Element of line_of_REAL n
for P being Element of plane_of_REAL n st L c= P & L1 c= P & L2 c= P & L _|_ L1 & L _|_ L2 holds
L1 // L2
proof end;

theorem Th112: :: EUCLIDLP:112
for n being Nat
for L, L0, L1, L2 being Element of line_of_REAL n
for P being Element of plane_of_REAL n st L0 c= P & L1 c= P & L2 c= P & L0 // L1 & L1 // L2 & L0 <> L1 & L meets L0 & L meets L1 holds
L meets L2
proof end;

theorem Th113: :: EUCLIDLP:113
for n being Nat
for L1, L2 being Element of line_of_REAL n st L1,L2 are_coplane & L1 is being_line & L2 is being_line & L1 misses L2 holds
L1 // L2
proof end;

theorem :: EUCLIDLP:114
for n being Nat
for x1, x2, y1, y2 being Element of REAL n
for P being Element of plane_of_REAL n st x1 in P & x2 in P & y1 in P & y2 in P & x2 - x1,y2 - y1 are_lindependent2 holds
Line (x1,x2) meets Line (y1,y2)
proof end;