begin
Lm1:
for AS being AffinSpace
for X being Subset of
for x being set st x in X holds
x is Element of
;
theorem Th1:
for
AS being
AffinSpace for
p,
a,
a',
b being
Element of st (
LIN p,
a,
a' or
LIN p,
a',
a ) &
p <> a holds
ex
b' being
Element of st
(
LIN p,
b,
b' &
a,
b // a',
b' )
theorem Th2:
theorem Th3:
theorem Th4:
for
AS being
AffinSpace for
a,
b,
c,
d being
Element of
for
A being
Subset of st (
a,
b // A or
b,
a // A ) & (
a,
b // c,
d or
c,
d // a,
b ) &
a <> b holds
(
c,
d // A &
d,
c // A )
theorem
theorem
theorem Th7:
Lm2:
for AS being AffinSpace
for a, a', d being Element of
for A, K being Subset of st A // K & a in A & a' in A & d in K holds
ex d' being Element of st
( d' in K & a,d // a',d' )
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
:: deftheorem defines Plane AFF_4:def 1 :
:: deftheorem Def2 defines being_plane AFF_4:def 2 :
Lm3:
for AS being AffinSpace
for K, P being Subset of
for q being Element of holds
( q in Plane K,P iff ex b being Element of st
( q,b // K & b in P ) )
theorem
theorem Th14:
theorem
theorem Th16:
theorem
theorem Th18:
Lm4:
for AS being AffinSpace
for a being Element of
for Q, K, P being Subset of st a in Q & a in Plane K,P & K // Q holds
Q c= Plane K,P
Lm5:
for AS being AffinSpace
for a, b being Element of
for K, P, Q being Subset of st K is being_line & P is being_line & Q is being_line & a in Plane K,P & b in Plane K,P & a <> b & a in Q & b in Q holds
Q c= Plane K,P
theorem Th19:
Lm6:
for AS being AffinSpace
for K, Q, P being Subset of st K is being_line & Q c= Plane K,P holds
Plane K,Q c= Plane K,P
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
theorem Th24:
theorem Th25:
Lm7:
for AS being AffinSpace
for a, b, c being Element of
for M being Subset of st M is being_line & a in M & b in M & a <> b & not c in M holds
not LIN a,b,c
theorem Th26:
:: deftheorem Def3 defines * AFF_4:def 3 :
theorem Th27:
theorem Th28:
theorem Th29:
theorem
theorem Th31:
Lm8:
for AS being AffinSpace
for a being Element of
for A being Subset of st A is being_line & a in A holds
a * A = A
theorem Th32:
:: deftheorem Def4 defines '||' AFF_4:def 4 :
theorem Th33:
theorem Th34:
Lm9:
for AS being AffinSpace
for a being Element of
for X being Subset of st X is being_plane holds
ex b, c being Element of st
( b in X & c in X & not LIN a,b,c )
theorem
theorem Th36:
theorem Th37:
theorem Th38:
theorem Th39:
theorem
theorem Th41:
theorem
theorem
:: deftheorem Def5 defines is_coplanar AFF_4:def 5 :
theorem Th44:
for
AS being
AffinSpace for
K,
M,
N being
Subset of st
K,
M,
N is_coplanar holds
(
K,
N,
M is_coplanar &
M,
K,
N is_coplanar &
M,
N,
K is_coplanar &
N,
K,
M is_coplanar &
N,
M,
K is_coplanar )
theorem
theorem Th46:
theorem Th47:
theorem Th48:
Lm10:
for AS being AffinSpace
for q, a, b, c, a', b', c' being Element of
for A, P, C being Subset of st q in A & q in P & q in C & not A,P,C is_coplanar & q <> a & q <> b & q <> c & a in A & a' in A & b in P & b' in P & c in C & c' in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a',b' & a,c // a',c' holds
b,c // b',c'
theorem Th49:
for
AS being
AffinSpace for
q,
a,
b,
c,
a',
b',
c' being
Element of
for
A,
P,
C being
Subset of st
AS is not
AffinPlane &
q in A &
q in P &
q in C &
q <> a &
q <> b &
q <> c &
a in A &
a' in A &
b in P &
b' in P &
c in C &
c' in C &
A is
being_line &
P is
being_line &
C is
being_line &
A <> P &
A <> C &
a,
b // a',
b' &
a,
c // a',
c' holds
b,
c // b',
c'
theorem
Lm11:
for AS being AffinSpace
for a, a', b, b', c, c' being Element of
for A, P, C being Subset of st A // P & A // C & not A,P,C is_coplanar & a in A & a' in A & b in P & b' in P & c in C & c' in C & A is being_line & A <> P & A <> C & a,b // a',b' & a,c // a',c' holds
b,c // b',c'
theorem Th51:
for
AS being
AffinSpace for
a,
a',
b,
b',
c,
c' being
Element of
for
A,
P,
C being
Subset of st
AS is not
AffinPlane &
A // P &
A // C &
a in A &
a' in A &
b in P &
b' in P &
c in C &
c' in C &
A is
being_line &
P is
being_line &
C is
being_line &
A <> P &
A <> C &
a,
b // a',
b' &
a,
c // a',
c' holds
b,
c // b',
c'
theorem
theorem Th53:
for
AS being
AffinSpace for
a,
b,
c,
a',
b' being
Element of st
AS is
AffinPlane & not
LIN a,
b,
c holds
ex
c' being
Element of st
(
a,
c // a',
c' &
b,
c // b',
c' )
Lm12:
for AS being AffinSpace
for a, b, c, a', b' being Element of
for X being Subset of st not LIN a,b,c & a,b // a',b' & a in X & b in X & c in X & X is being_plane & a' in X holds
ex c' being Element of st
( a,c // a',c' & b,c // b',c' )
theorem Th54:
for
AS being
AffinSpace for
a,
b,
c,
a',
b' being
Element of st not
LIN a,
b,
c &
a' <> b' &
a,
b // a',
b' holds
ex
c' being
Element of st
(
a,
c // a',
c' &
b,
c // b',
c' )
theorem Th55:
theorem
theorem Th57:
theorem Th58:
theorem Th59:
theorem Th60:
theorem Th61:
Lm13:
for AS being AffinSpace
for X, Y being Subset of st X is being_plane & Y is being_plane & X '||' Y & X <> Y holds
for a being Element of holds
( not a in X or not a in Y )
theorem
theorem Th63:
theorem
theorem Th65:
:: deftheorem Def6 defines + AFF_4:def 6 :
theorem
theorem
theorem
theorem