:: by Wojciech Leo\'nczuk, Henryk Oryszczyszyn and Krzysztof Pra\.zmowski

::

:: Received December 5, 1990

:: Copyright (c) 1990-2021 Association of Mizar Users

Lm1: for AS being AffinSpace

for X being Subset of AS

for x being set st x in X holds

x is Element of AS

;

theorem Th1: :: AFF_4:1

for AS being AffinSpace

for a, b, a9, p being Element of AS st ( LIN p,a,a9 or LIN p,a9,a ) & p <> a holds

ex b9 being Element of AS st

( LIN p,b,b9 & a,b // a9,b9 )

for a, b, a9, p being Element of AS st ( LIN p,a,a9 or LIN p,a9,a ) & p <> a holds

ex b9 being Element of AS st

( LIN p,b,b9 & a,b // a9,b9 )

proof end;

theorem Th2: :: AFF_4:2

for AS being AffinSpace

for a, b being Element of AS

for A being Subset of AS st ( a,b // A or b,a // A ) & a in A holds

b in A

for a, b being Element of AS

for A being Subset of AS st ( a,b // A or b,a // A ) & a in A holds

b in A

proof end;

theorem Th3: :: AFF_4:3

for AS being AffinSpace

for a, b being Element of AS

for A, K being Subset of AS st ( a,b // A or b,a // A ) & A // K holds

( a,b // K & b,a // K )

for a, b being Element of AS

for A, K being Subset of AS st ( a,b // A or b,a // A ) & A // K holds

( a,b // K & b,a // K )

proof end;

theorem Th4: :: AFF_4:4

for AS being AffinSpace

for a, b, c, d being Element of AS

for A being Subset of AS 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 )

for a, b, c, d being Element of AS

for A being Subset of AS 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 )

proof end;

theorem :: AFF_4:5

for AS being AffinSpace

for a, b being Element of AS

for M, N being Subset of AS st ( a,b // M or b,a // M ) & ( a,b // N or b,a // N ) & a <> b holds

M // N

for a, b being Element of AS

for M, N being Subset of AS st ( a,b // M or b,a // M ) & ( a,b // N or b,a // N ) & a <> b holds

M // N

proof end;

theorem :: AFF_4:6

for AS being AffinSpace

for a, b, c, d being Element of AS

for M being Subset of AS st ( a,b // M or b,a // M ) & ( c,d // M or d,c // M ) holds

a,b // c,d

for a, b, c, d being Element of AS

for M being Subset of AS st ( a,b // M or b,a // M ) & ( c,d // M or d,c // M ) holds

a,b // c,d

proof end;

theorem Th7: :: AFF_4:7

for AS being AffinSpace

for a, b, c, d being Element of AS

for A, C being Subset of AS st ( A // C or C // A ) & a <> b & ( a,b // c,d or c,d // a,b ) & a in A & b in A & c in C holds

d in C

for a, b, c, d being Element of AS

for A, C being Subset of AS st ( A // C or C // A ) & a <> b & ( a,b // c,d or c,d // a,b ) & a in A & b in A & c in C holds

d in C

proof end;

Lm2: for AS being AffinSpace

for a, d, a9 being Element of AS

for A, K being Subset of AS st A // K & a in A & a9 in A & d in K holds

ex d9 being Element of AS st

( d9 in K & a,d // a9,d9 )

proof end;

theorem Th8: :: AFF_4:8

for AS being AffinSpace

for a, b, a9, b9, q being Element of AS

for M, N being Subset of AS st q in M & q in N & a in M & b in N & b9 in N & q <> a & q <> b & M <> N & ( a,b // a9,b9 or b,a // b9,a9 ) & M is being_line & N is being_line & q = a9 holds

q = b9

for a, b, a9, b9, q being Element of AS

for M, N being Subset of AS st q in M & q in N & a in M & b in N & b9 in N & q <> a & q <> b & M <> N & ( a,b // a9,b9 or b,a // b9,a9 ) & M is being_line & N is being_line & q = a9 holds

q = b9

proof end;

theorem Th9: :: AFF_4:9

for AS being AffinSpace

for a, b, a9, b9, q being Element of AS

for M, N being Subset of AS st q in M & q in N & a in M & a9 in M & b in N & b9 in N & q <> a & q <> b & M <> N & ( a,b // a9,b9 or b,a // b9,a9 ) & M is being_line & N is being_line & a = a9 holds

b = b9

for a, b, a9, b9, q being Element of AS

for M, N being Subset of AS st q in M & q in N & a in M & a9 in M & b in N & b9 in N & q <> a & q <> b & M <> N & ( a,b // a9,b9 or b,a // b9,a9 ) & M is being_line & N is being_line & a = a9 holds

b = b9

proof end;

theorem Th10: :: AFF_4:10

for AS being AffinSpace

for a, b, a9, b9 being Element of AS

for M, N being Subset of AS st ( M // N or N // M ) & a in M & b in N & b9 in N & M <> N & ( a,b // a9,b9 or b,a // b9,a9 ) & a = a9 holds

b = b9

for a, b, a9, b9 being Element of AS

for M, N being Subset of AS st ( M // N or N // M ) & a in M & b in N & b9 in N & M <> N & ( a,b // a9,b9 or b,a // b9,a9 ) & a = a9 holds

b = b9

proof end;

theorem Th11: :: AFF_4:11

for AS being AffinSpace

for a, b being Element of AS ex A being Subset of AS st

( a in A & b in A & A is being_line )

for a, b being Element of AS ex A being Subset of AS st

( a in A & b in A & A is being_line )

proof end;

theorem Th12: :: AFF_4:12

for AS being AffinSpace

for A being Subset of AS st A is being_line holds

ex q being Element of AS st not q in A

for A being Subset of AS st A is being_line holds

ex q being Element of AS st not q in A

proof end;

definition

let AS be AffinSpace;

let K, P be Subset of AS;

{ a where a is Element of AS : ex b being Element of AS st

( a,b // K & b in P ) } is Subset of AS

end;
let K, P be Subset of AS;

func Plane (K,P) -> Subset of AS equals :: AFF_4:def 1

{ a where a is Element of AS : ex b being Element of AS st

( a,b // K & b in P ) } ;

coherence { a where a is Element of AS : ex b being Element of AS st

( a,b // K & b in P ) } ;

{ a where a is Element of AS : ex b being Element of AS st

( a,b // K & b in P ) } is Subset of AS

proof end;

:: deftheorem defines Plane AFF_4:def 1 :

for AS being AffinSpace

for K, P being Subset of AS holds Plane (K,P) = { a where a is Element of AS : ex b being Element of AS st

( a,b // K & b in P ) } ;

for AS being AffinSpace

for K, P being Subset of AS holds Plane (K,P) = { a where a is Element of AS : ex b being Element of AS st

( a,b // K & b in P ) } ;

definition

let AS be AffinSpace;

let X be Subset of AS;

end;
let X be Subset of AS;

attr X is being_plane means :: AFF_4:def 2

ex K, P being Subset of AS st

( K is being_line & P is being_line & not K // P & X = Plane (K,P) );

ex K, P being Subset of AS st

( K is being_line & P is being_line & not K // P & X = Plane (K,P) );

:: deftheorem defines being_plane AFF_4:def 2 :

for AS being AffinSpace

for X being Subset of AS holds

( X is being_plane iff ex K, P being Subset of AS st

( K is being_line & P is being_line & not K // P & X = Plane (K,P) ) );

for AS being AffinSpace

for X being Subset of AS holds

( X is being_plane iff ex K, P being Subset of AS st

( K is being_line & P is being_line & not K // P & X = Plane (K,P) ) );

Lm3: for AS being AffinSpace

for K, P being Subset of AS

for q being Element of AS holds

( q in Plane (K,P) iff ex b being Element of AS st

( q,b // K & b in P ) )

proof end;

theorem :: AFF_4:17

for AS being AffinSpace

for a, b, a9, b9, p being Element of AS

for M, N, P, Q being Subset of AS st p in M & a in M & b in M & p in N & a9 in N & b9 in N & not p in P & not p in Q & M <> N & a in P & a9 in P & b in Q & b9 in Q & M is being_line & N is being_line & P is being_line & Q is being_line & not P // Q holds

ex q being Element of AS st

( q in P & q in Q )

for a, b, a9, b9, p being Element of AS

for M, N, P, Q being Subset of AS st p in M & a in M & b in M & p in N & a9 in N & b9 in N & not p in P & not p in Q & M <> N & a in P & a9 in P & b in Q & b9 in Q & M is being_line & N is being_line & P is being_line & Q is being_line & not P // Q holds

ex q being Element of AS st

( q in P & q in Q )

proof end;

theorem Th18: :: AFF_4:18

for AS being AffinSpace

for a, b, a9, b9 being Element of AS

for M, N, P, Q being Subset of AS st a in M & b in M & a9 in N & b9 in N & a in P & a9 in P & b in Q & b9 in Q & M <> N & M // N & P is being_line & Q is being_line & not P // Q holds

ex q being Element of AS st

( q in P & q in Q )

for a, b, a9, b9 being Element of AS

for M, N, P, Q being Subset of AS st a in M & b in M & a9 in N & b9 in N & a in P & a9 in P & b in Q & b9 in Q & M <> N & M // N & P is being_line & Q is being_line & not P // Q holds

ex q being Element of AS st

( q in P & q in Q )

proof end;

Lm4: for AS being AffinSpace

for a being Element of AS

for K, P, Q being Subset of AS st a in Q & a in Plane (K,P) & K // Q holds

Q c= Plane (K,P)

proof end;

Lm5: for AS being AffinSpace

for a, b being Element of AS

for K, P, Q being Subset of AS 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)

proof end;

theorem Th19: :: AFF_4:19

for AS being AffinSpace

for a, b being Element of AS

for X being Subset of AS st X is being_plane & a in X & b in X & a <> b holds

Line (a,b) c= X

for a, b being Element of AS

for X being Subset of AS st X is being_plane & a in X & b in X & a <> b holds

Line (a,b) c= X

proof end;

Lm6: for AS being AffinSpace

for K, P, Q being Subset of AS st K is being_line & Q c= Plane (K,P) holds

Plane (K,Q) c= Plane (K,P)

proof end;

theorem Th20: :: AFF_4:20

for AS being AffinSpace

for K, P, Q being Subset of AS st K is being_line & P is being_line & Q is being_line & not K // Q & Q c= Plane (K,P) holds

Plane (K,Q) = Plane (K,P)

for K, P, Q being Subset of AS st K is being_line & P is being_line & Q is being_line & not K // Q & Q c= Plane (K,P) holds

Plane (K,Q) = Plane (K,P)

proof end;

theorem Th21: :: AFF_4:21

for AS being AffinSpace

for K, P, Q being Subset of AS st K is being_line & P is being_line & Q is being_line & Q c= Plane (K,P) & not P // Q holds

ex q being Element of AS st

( q in P & q in Q )

for K, P, Q being Subset of AS st K is being_line & P is being_line & Q is being_line & Q c= Plane (K,P) & not P // Q holds

ex q being Element of AS st

( q in P & q in Q )

proof end;

theorem Th22: :: AFF_4:22

for AS being AffinSpace

for M, N, X being Subset of AS st X is being_plane & M is being_line & N is being_line & M c= X & N c= X & not M // N holds

ex q being Element of AS st

( q in M & q in N )

for M, N, X being Subset of AS st X is being_plane & M is being_line & N is being_line & M c= X & N c= X & not M // N holds

ex q being Element of AS st

( q in M & q in N )

proof end;

theorem Th23: :: AFF_4:23

for AS being AffinSpace

for a being Element of AS

for M, N, X being Subset of AS st X is being_plane & a in X & M c= X & a in N & ( M // N or N // M ) holds

N c= X

for a being Element of AS

for M, N, X being Subset of AS st X is being_plane & a in X & M c= X & a in N & ( M // N or N // M ) holds

N c= X

proof end;

theorem Th24: :: AFF_4:24

for AS being AffinSpace

for a, b being Element of AS

for X, Y being Subset of AS st X is being_plane & Y is being_plane & a in X & b in X & a in Y & b in Y & X <> Y & a <> b holds

X /\ Y is being_line

for a, b being Element of AS

for X, Y being Subset of AS st X is being_plane & Y is being_plane & a in X & b in X & a in Y & b in Y & X <> Y & a <> b holds

X /\ Y is being_line

proof end;

theorem Th25: :: AFF_4:25

for AS being AffinSpace

for a, b, c being Element of AS

for X, Y being Subset of AS st X is being_plane & Y is being_plane & a in X & b in X & c in X & a in Y & b in Y & c in Y & not LIN a,b,c holds

X = Y

for a, b, c being Element of AS

for X, Y being Subset of AS st X is being_plane & Y is being_plane & a in X & b in X & c in X & a in Y & b in Y & c in Y & not LIN a,b,c holds

X = Y

proof end;

Lm7: for AS being AffinSpace

for a, b, c being Element of AS

for M being Subset of AS st M is being_line & a in M & b in M & a <> b & not c in M holds

not LIN a,b,c

proof end;

theorem Th26: :: AFF_4:26

for AS being AffinSpace

for M, N, X, Y being Subset of AS st X is being_plane & Y is being_plane & M is being_line & N is being_line & M c= X & N c= X & M c= Y & N c= Y & M <> N holds

X = Y

for M, N, X, Y being Subset of AS st X is being_plane & Y is being_plane & M is being_line & N is being_line & M c= X & N c= X & M c= Y & N c= Y & M <> N holds

X = Y

proof end;

definition

let AS be AffinSpace;

let a be Element of AS;

let K be Subset of AS;

assume A1: K is being_line ;

existence

ex b_{1} being Subset of AS st

( a in b_{1} & K // b_{1} )
by A1, AFF_1:49;

uniqueness

for b_{1}, b_{2} being Subset of AS st a in b_{1} & K // b_{1} & a in b_{2} & K // b_{2} holds

b_{1} = b_{2}
by AFF_1:50;

end;
let a be Element of AS;

let K be Subset of AS;

assume A1: K is being_line ;

existence

ex b

( a in b

uniqueness

for b

b

:: deftheorem Def3 defines * AFF_4:def 3 :

for AS being AffinSpace

for a being Element of AS

for K being Subset of AS st K is being_line holds

for b_{4} being Subset of AS holds

( b_{4} = a * K iff ( a in b_{4} & K // b_{4} ) );

for AS being AffinSpace

for a being Element of AS

for K being Subset of AS st K is being_line holds

for b

( b

theorem Th27: :: AFF_4:27

for AS being AffinSpace

for a being Element of AS

for A being Subset of AS st A is being_line holds

a * A is being_line

for a being Element of AS

for A being Subset of AS st A is being_line holds

a * A is being_line

proof end;

theorem Th28: :: AFF_4:28

for AS being AffinSpace

for a being Element of AS

for M, X being Subset of AS st X is being_plane & M is being_line & a in X & M c= X holds

a * M c= X

for a being Element of AS

for M, X being Subset of AS st X is being_plane & M is being_line & a in X & M c= X holds

a * M c= X

proof end;

theorem Th29: :: AFF_4:29

for AS being AffinSpace

for a, b, c, d being Element of AS

for X being Subset of AS st X is being_plane & a in X & b in X & c in X & a,b // c,d & a <> b holds

d in X

for a, b, c, d being Element of AS

for X being Subset of AS st X is being_plane & a in X & b in X & c in X & a,b // c,d & a <> b holds

d in X

proof end;

theorem :: AFF_4:30

for AS being AffinSpace

for a being Element of AS

for A being Subset of AS st A is being_line holds

( a in A iff a * A = A )

for a being Element of AS

for A being Subset of AS st A is being_line holds

( a in A iff a * A = A )

proof end;

theorem Th31: :: AFF_4:31

for AS being AffinSpace

for a, q being Element of AS

for A being Subset of AS st A is being_line holds

a * A = a * (q * A)

for a, q being Element of AS

for A being Subset of AS st A is being_line holds

a * A = a * (q * A)

proof end;

Lm8: for AS being AffinSpace

for a being Element of AS

for A being Subset of AS st A is being_line & a in A holds

a * A = A

proof end;

theorem Th32: :: AFF_4:32

for AS being AffinSpace

for a being Element of AS

for K, M being Subset of AS st K // M holds

a * K = a * M

for a being Element of AS

for K, M being Subset of AS st K // M holds

a * K = a * M

proof end;

definition

let AS be AffinSpace;

let X, Y be Subset of AS;

end;
let X, Y be Subset of AS;

pred X '||' Y means :: AFF_4:def 4

for a being Element of AS

for A being Subset of AS st a in Y & A is being_line & A c= X holds

a * A c= Y;

for a being Element of AS

for A being Subset of AS st a in Y & A is being_line & A c= X holds

a * A c= Y;

:: deftheorem defines '||' AFF_4:def 4 :

for AS being AffinSpace

for X, Y being Subset of AS holds

( X '||' Y iff for a being Element of AS

for A being Subset of AS st a in Y & A is being_line & A c= X holds

a * A c= Y );

for AS being AffinSpace

for X, Y being Subset of AS holds

( X '||' Y iff for a being Element of AS

for A being Subset of AS st a in Y & A is being_line & A c= X holds

a * A c= Y );

theorem Th33: :: AFF_4:33

for AS being AffinSpace

for X, Y being Subset of AS st X c= Y & ( ( X is being_line & Y is being_line ) or ( X is being_plane & Y is being_plane ) ) holds

X = Y

for X, Y being Subset of AS st X c= Y & ( ( X is being_line & Y is being_line ) or ( X is being_plane & Y is being_plane ) ) holds

X = Y

proof end;

theorem Th34: :: AFF_4:34

for AS being AffinSpace

for X being Subset of AS st X is being_plane holds

ex a, b, c being Element of AS st

( a in X & b in X & c in X & not LIN a,b,c )

for X being Subset of AS st X is being_plane holds

ex a, b, c being Element of AS st

( a in X & b in X & c in X & not LIN a,b,c )

proof end;

Lm9: for AS being AffinSpace

for a being Element of AS

for X being Subset of AS st X is being_plane holds

ex b, c being Element of AS st

( b in X & c in X & not LIN a,b,c )

proof end;

theorem :: AFF_4:35

for AS being AffinSpace

for M, X being Subset of AS st M is being_line & X is being_plane holds

ex q being Element of AS st

( q in X & not q in M )

for M, X being Subset of AS st M is being_line & X is being_plane holds

ex q being Element of AS st

( q in X & not q in M )

proof end;

theorem Th36: :: AFF_4:36

for AS being AffinSpace

for a being Element of AS

for A being Subset of AS st A is being_line holds

ex X being Subset of AS st

( a in X & A c= X & X is being_plane )

for a being Element of AS

for A being Subset of AS st A is being_line holds

ex X being Subset of AS st

( a in X & A c= X & X is being_plane )

proof end;

theorem Th37: :: AFF_4:37

for AS being AffinSpace

for a, b, c being Element of AS ex X being Subset of AS st

( a in X & b in X & c in X & X is being_plane )

for a, b, c being Element of AS ex X being Subset of AS st

( a in X & b in X & c in X & X is being_plane )

proof end;

theorem Th38: :: AFF_4:38

for AS being AffinSpace

for q being Element of AS

for M, N being Subset of AS st q in M & q in N & M is being_line & N is being_line holds

ex X being Subset of AS st

( M c= X & N c= X & X is being_plane )

for q being Element of AS

for M, N being Subset of AS st q in M & q in N & M is being_line & N is being_line holds

ex X being Subset of AS st

( M c= X & N c= X & X is being_plane )

proof end;

theorem Th39: :: AFF_4:39

for AS being AffinSpace

for M, N being Subset of AS st M // N holds

ex X being Subset of AS st

( M c= X & N c= X & X is being_plane )

for M, N being Subset of AS st M // N holds

ex X being Subset of AS st

( M c= X & N c= X & X is being_plane )

proof end;

theorem :: AFF_4:40

for AS being AffinSpace

for M, N being Subset of AS st M is being_line & N is being_line holds

( M // N iff M '||' N )

for M, N being Subset of AS st M is being_line & N is being_line holds

( M // N iff M '||' N )

proof end;

theorem Th41: :: AFF_4:41

for AS being AffinSpace

for M, X being Subset of AS st M is being_line & X is being_plane holds

( M '||' X iff ex N being Subset of AS st

( N c= X & ( M // N or N // M ) ) )

for M, X being Subset of AS st M is being_line & X is being_plane holds

( M '||' X iff ex N being Subset of AS st

( N c= X & ( M // N or N // M ) ) )

proof end;

theorem :: AFF_4:42

for AS being AffinSpace

for M, X being Subset of AS st M is being_line & X is being_plane & M c= X holds

M '||' X

for M, X being Subset of AS st M is being_line & X is being_plane & M c= X holds

M '||' X

proof end;

theorem :: AFF_4:43

for AS being AffinSpace

for a being Element of AS

for A, X being Subset of AS st A is being_line & X is being_plane & a in A & a in X & A '||' X holds

A c= X

for a being Element of AS

for A, X being Subset of AS st A is being_line & X is being_plane & a in A & a in X & A '||' X holds

A c= X

proof end;

definition

let AS be AffinSpace;

let K, M, N be Subset of AS;

end;
let K, M, N be Subset of AS;

pred K,M,N is_coplanar means :: AFF_4:def 5

ex X being Subset of AS st

( K c= X & M c= X & N c= X & X is being_plane );

ex X being Subset of AS st

( K c= X & M c= X & N c= X & X is being_plane );

:: deftheorem defines is_coplanar AFF_4:def 5 :

for AS being AffinSpace

for K, M, N being Subset of AS holds

( K,M,N is_coplanar iff ex X being Subset of AS st

( K c= X & M c= X & N c= X & X is being_plane ) );

for AS being AffinSpace

for K, M, N being Subset of AS holds

( K,M,N is_coplanar iff ex X being Subset of AS st

( K c= X & M c= X & N c= X & X is being_plane ) );

theorem :: AFF_4:44

for AS being AffinSpace

for K, M, N being Subset of AS 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 ) ;

for K, M, N being Subset of AS 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 :: AFF_4:45

for AS being AffinSpace

for A, K, M, N being Subset of AS st M is being_line & N is being_line & M,N,K is_coplanar & M,N,A is_coplanar & M <> N holds

M,K,A is_coplanar

for A, K, M, N being Subset of AS st M is being_line & N is being_line & M,N,K is_coplanar & M,N,A is_coplanar & M <> N holds

M,K,A is_coplanar

proof end;

theorem Th46: :: AFF_4:46

for AS being AffinSpace

for A, K, M, X being Subset of AS st K is being_line & M is being_line & X is being_plane & K c= X & M c= X & K <> M holds

( K,M,A is_coplanar iff A c= X ) by Th26;

for A, K, M, X being Subset of AS st K is being_line & M is being_line & X is being_plane & K c= X & M c= X & K <> M holds

( K,M,A is_coplanar iff A c= X ) by Th26;

theorem Th47: :: AFF_4:47

for AS being AffinSpace

for q being Element of AS

for K, M being Subset of AS st q in K & q in M & K is being_line & M is being_line holds

( K,M,M is_coplanar & M,K,M is_coplanar & M,M,K is_coplanar )

for q being Element of AS

for K, M being Subset of AS st q in K & q in M & K is being_line & M is being_line holds

( K,M,M is_coplanar & M,K,M is_coplanar & M,M,K is_coplanar )

proof end;

theorem Th48: :: AFF_4:48

for AS being AffinSpace

for X being Subset of AS st AS is not AffinPlane & X is being_plane holds

ex q being Element of AS st not q in X

for X being Subset of AS st AS is not AffinPlane & X is being_plane holds

ex q being Element of AS st not q in X

proof end;

Lm10: for AS being AffinSpace

for a, b, c, a9, b9, c9, q being Element of AS

for A, C, P being Subset of AS 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 & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 holds

b,c // b9,c9

proof end;

theorem Th49: :: AFF_4:49

for AS being AffinSpace

for a, b, c, a9, b9, c9, q being Element of AS

for A, C, P being Subset of AS st AS is not AffinPlane & q in A & q in P & q in C & q <> a & q <> b & q <> c & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 holds

b,c // b9,c9

for a, b, c, a9, b9, c9, q being Element of AS

for A, C, P being Subset of AS st AS is not AffinPlane & q in A & q in P & q in C & q <> a & q <> b & q <> c & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 holds

b,c // b9,c9

proof end;

Lm11: for AS being AffinSpace

for a, b, c, a9, b9, c9 being Element of AS

for A, C, P being Subset of AS st A // P & A // C & not A,P,C is_coplanar & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 holds

b,c // b9,c9

proof end;

theorem Th51: :: AFF_4:51

for AS being AffinSpace

for a, b, c, a9, b9, c9 being Element of AS

for A, C, P being Subset of AS st AS is not AffinPlane & A // P & A // C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 holds

b,c // b9,c9

for a, b, c, a9, b9, c9 being Element of AS

for A, C, P being Subset of AS st AS is not AffinPlane & A // P & A // C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 holds

b,c // b9,c9

proof end;

theorem Th53: :: AFF_4:53

for AS being AffinSpace

for a, b, c, a9, b9 being Element of AS st AS is AffinPlane & not LIN a,b,c holds

ex c9 being Element of AS st

( a,c // a9,c9 & b,c // b9,c9 )

for a, b, c, a9, b9 being Element of AS st AS is AffinPlane & not LIN a,b,c holds

ex c9 being Element of AS st

( a,c // a9,c9 & b,c // b9,c9 )

proof end;

Lm12: for AS being AffinSpace

for a, b, c, a9, b9 being Element of AS

for X being Subset of AS st not LIN a,b,c & a,b // a9,b9 & a in X & b in X & c in X & X is being_plane & a9 in X holds

ex c9 being Element of AS st

( a,c // a9,c9 & b,c // b9,c9 )

proof end;

theorem Th54: :: AFF_4:54

for AS being AffinSpace

for a, b, c, a9, b9 being Element of AS st not LIN a,b,c & a9 <> b9 & a,b // a9,b9 holds

ex c9 being Element of AS st

( a,c // a9,c9 & b,c // b9,c9 )

for a, b, c, a9, b9 being Element of AS st not LIN a,b,c & a9 <> b9 & a,b // a9,b9 holds

ex c9 being Element of AS st

( a,c // a9,c9 & b,c // b9,c9 )

proof end;

theorem Th55: :: AFF_4:55

for AS being AffinSpace

for X, Y being Subset of AS st X is being_plane & Y is being_plane holds

( X '||' Y iff ex A, P, M, N being Subset of AS st

( not A // P & A c= X & P c= X & M c= Y & N c= Y & ( A // M or M // A ) & ( P // N or N // P ) ) )

for X, Y being Subset of AS st X is being_plane & Y is being_plane holds

( X '||' Y iff ex A, P, M, N being Subset of AS st

( not A // P & A c= X & P c= X & M c= Y & N c= Y & ( A // M or M // A ) & ( P // N or N // P ) ) )

proof end;

theorem Th58: :: AFF_4:58

for AS being AffinSpace

for X, Y being Subset of AS st X is being_plane & Y is being_plane & X '||' Y holds

Y '||' X

for X, Y being Subset of AS st X is being_plane & Y is being_plane & X '||' Y holds

Y '||' X

proof end;

theorem Th60: :: AFF_4:60

for AS being AffinSpace

for X, Y, Z being Subset of AS st X '||' Y & Y '||' Z & Y <> {} holds

X '||' Z

for X, Y, Z being Subset of AS st X '||' Y & Y '||' Z & Y <> {} holds

X '||' Z

proof end;

theorem Th61: :: AFF_4:61

for AS being AffinSpace

for X, Y, Z being Subset of AS st X is being_plane & Y is being_plane & Z is being_plane & ( ( X '||' Y & Y '||' Z ) or ( X '||' Y & Z '||' Y ) or ( Y '||' X & Y '||' Z ) or ( Y '||' X & Z '||' Y ) ) holds

X '||' Z

for X, Y, Z being Subset of AS st X is being_plane & Y is being_plane & Z is being_plane & ( ( X '||' Y & Y '||' Z ) or ( X '||' Y & Z '||' Y ) or ( Y '||' X & Y '||' Z ) or ( Y '||' X & Z '||' Y ) ) holds

X '||' Z

proof end;

Lm13: for AS being AffinSpace

for X, Y being Subset of AS st X is being_plane & Y is being_plane & X '||' Y & X <> Y holds

for a being Element of AS holds

( not a in X or not a in Y )

proof end;

theorem :: AFF_4:62

for AS being AffinSpace

for a being Element of AS

for X, Y being Subset of AS st X is being_plane & Y is being_plane & a in X & a in Y & X '||' Y holds

X = Y by Lm13;

for a being Element of AS

for X, Y being Subset of AS st X is being_plane & Y is being_plane & a in X & a in Y & X '||' Y holds

X = Y by Lm13;

theorem Th63: :: AFF_4:63

for AS being AffinSpace

for a, b, c, d being Element of AS

for X, Y, Z being Subset of AS st X is being_plane & Y is being_plane & Z is being_plane & X '||' Y & X <> Y & a in X /\ Z & b in X /\ Z & c in Y /\ Z & d in Y /\ Z holds

a,b // c,d

for a, b, c, d being Element of AS

for X, Y, Z being Subset of AS st X is being_plane & Y is being_plane & Z is being_plane & X '||' Y & X <> Y & a in X /\ Z & b in X /\ Z & c in Y /\ Z & d in Y /\ Z holds

a,b // c,d

proof end;

theorem :: AFF_4:64

for AS being AffinSpace

for a, b, c, d being Element of AS

for X, Y, Z being Subset of AS st X is being_plane & Y is being_plane & Z is being_plane & X '||' Y & a in X /\ Z & b in X /\ Z & c in Y /\ Z & d in Y /\ Z & X <> Y & a <> b & c <> d holds

X /\ Z // Y /\ Z

for a, b, c, d being Element of AS

for X, Y, Z being Subset of AS st X is being_plane & Y is being_plane & Z is being_plane & X '||' Y & a in X /\ Z & b in X /\ Z & c in Y /\ Z & d in Y /\ Z & X <> Y & a <> b & c <> d holds

X /\ Z // Y /\ Z

proof end;

theorem Th65: :: AFF_4:65

for AS being AffinSpace

for a being Element of AS

for X being Subset of AS st X is being_plane holds

ex Y being Subset of AS st

( a in Y & X '||' Y & Y is being_plane )

for a being Element of AS

for X being Subset of AS st X is being_plane holds

ex Y being Subset of AS st

( a in Y & X '||' Y & Y is being_plane )

proof end;

definition

let AS be AffinSpace;

let a be Element of AS;

let X be Subset of AS;

assume A1: X is being_plane ;

existence

ex b_{1} being Subset of AS st

( a in b_{1} & X '||' b_{1} & b_{1} is being_plane )
by A1, Th65;

uniqueness

for b_{1}, b_{2} being Subset of AS st a in b_{1} & X '||' b_{1} & b_{1} is being_plane & a in b_{2} & X '||' b_{2} & b_{2} is being_plane holds

b_{1} = b_{2}

end;
let a be Element of AS;

let X be Subset of AS;

assume A1: X is being_plane ;

existence

ex b

( a in b

uniqueness

for b

b

proof end;

:: deftheorem Def6 defines + AFF_4:def 6 :

for AS being AffinSpace

for a being Element of AS

for X being Subset of AS st X is being_plane holds

for b_{4} being Subset of AS holds

( b_{4} = a + X iff ( a in b_{4} & X '||' b_{4} & b_{4} is being_plane ) );

for AS being AffinSpace

for a being Element of AS

for X being Subset of AS st X is being_plane holds

for b

( b

theorem :: AFF_4:66

for AS being AffinSpace

for a being Element of AS

for X being Subset of AS st X is being_plane holds

( a in X iff a + X = X )

for a being Element of AS

for X being Subset of AS st X is being_plane holds

( a in X iff a + X = X )

proof end;

theorem :: AFF_4:67

for AS being AffinSpace

for a, q being Element of AS

for X being Subset of AS st X is being_plane holds

a + X = a + (q + X)

for a, q being Element of AS

for X being Subset of AS st X is being_plane holds

a + X = a + (q + X)

proof end;

theorem :: AFF_4:68

for AS being AffinSpace

for a being Element of AS

for A, X being Subset of AS st A is being_line & X is being_plane & A '||' X holds

a * A c= a + X

for a being Element of AS

for A, X being Subset of AS st A is being_line & X is being_plane & A '||' X holds

a * A c= a + X

proof end;

theorem :: AFF_4:69

for AS being AffinSpace

for a being Element of AS

for X, Y being Subset of AS st X is being_plane & Y is being_plane & X '||' Y holds

a + X = a + Y

for a being Element of AS

for X, Y being Subset of AS st X is being_plane & Y is being_plane & X '||' Y holds

a + X = a + Y

proof end;