:: AFF_4 semantic presentation

begin

                        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 p, a, a9, b 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
let AS be AffinSpace; ::_thesis: for p, a, a9, b 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 )
let p, a, a9, b be Element of AS; ::_thesis: ( ( LIN p,a,a9 or LIN p,a9,a ) & p <> a implies ex b9 being Element of AS st
( LIN p,b,b9 & a,b // a9,b9 ) )
assume that
A1: ( LIN p,a,a9 or LIN p,a9,a ) and
A2: p <> a ; ::_thesis: ex b9 being Element of AS st
( LIN p,b,b9 & a,b // a9,b9 )
 LIN p,a,a9 by A1, AFF_1:6;
then  p,a // p,a9 by AFF_1:def_1;
then  a,p // p,a9 by AFF_1:4;
then consider b9 being Element of AS such that
A3: b,p // p,b9 and
A4: b,a // a9,b9 by A2, DIRAF:40;
 p,b // p,b9 by A3, AFF_1:4;
then A5: LIN p,b,b9 by AFF_1:def_1;
 a,b // a9,b9 by A4, AFF_1:4;
hence  ex b9 being Element of AS st
( LIN p,b,b9 & a,b // a9,b9 ) by A5; ::_thesis: verum
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
proof
let AS be AffinSpace; ::_thesis: 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
let a, b be Element of AS; ::_thesis: for A being Subset of AS st ( a,b // A or b,a // A ) & a in A holds
b in A
let A be Subset of AS; ::_thesis: ( ( a,b // A or b,a // A ) & a in A implies b in A )
assume that
A1: ( a,b // A or b,a // A ) and
A2: a in A ; ::_thesis: b in A
 ( a,b // A & A is being_line ) by A1, AFF_1:26, AFF_1:34;
hence  b in A by A2, AFF_1:23; ::_thesis: verum
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 )
proof
let AS be AffinSpace; ::_thesis: 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 )
let a, b be Element of AS; ::_thesis: for A, K being Subset of AS st ( a,b // A or b,a // A ) & A // K holds
( a,b // K & b,a // K )
let A, K be Subset of AS; ::_thesis: ( ( a,b // A or b,a // A ) & A // K implies ( a,b // K & b,a // K ) )
assume that
A1: ( a,b // A or b,a // A ) and
A2: A // K ; ::_thesis: ( a,b // K & b,a // K )
 a,b // A by A1, AFF_1:34;
hence  a,b // K by A2, AFF_1:43; ::_thesis: b,a // K
hence  b,a // K by AFF_1:34; ::_thesis: verum
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 )
proof
let AS be AffinSpace; ::_thesis: 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 )
let a, b, c, d be Element of AS; ::_thesis: 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 )
let A be Subset of AS; ::_thesis: ( ( a,b // A or b,a // A ) & ( a,b // c,d or c,d // a,b ) & a <> b implies ( c,d // A & d,c // A ) )
assume that
A1: ( ( a,b // A or b,a // A ) & ( a,b // c,d or c,d // a,b ) ) and
A2: a <> b ; ::_thesis: ( c,d // A & d,c // A )
 ( a,b // A & a,b // c,d ) by A1, AFF_1:4, AFF_1:34;
hence  c,d // A by A2, AFF_1:32; ::_thesis: d,c // A
hence  d,c // A by AFF_1:34; ::_thesis: verum
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
proof
let AS be AffinSpace; ::_thesis: 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
let a, b be Element of AS; ::_thesis: 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
let M, N be Subset of AS; ::_thesis: ( ( a,b // M or b,a // M ) & ( a,b // N or b,a // N ) & a <> b implies M // N )
assume that
A1: ( ( a,b // M or b,a // M ) & ( a,b // N or b,a // N ) ) and
A2: a <> b ; ::_thesis: M // N
 ( a,b // M & a,b // N ) by A1, AFF_1:34;
hence  M // N by A2, AFF_1:53; ::_thesis: verum
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
proof
let AS be AffinSpace; ::_thesis: 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
let a, b, c, d be Element of AS; ::_thesis: 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
let M be Subset of AS; ::_thesis: ( ( a,b // M or b,a // M ) & ( c,d // M or d,c // M ) implies a,b // c,d )
assume  ( ( a,b // M or b,a // M ) & ( c,d // M or d,c // M ) ) ; ::_thesis: a,b // c,d
then A1: ( a,b // M & c,d // M ) by AFF_1:34;
then  M is being_line by AFF_1:26;
hence  a,b // c,d by A1, AFF_1:31; ::_thesis: verum
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
proof
let AS be AffinSpace; ::_thesis: 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
let a, b, c, d be Element of AS; ::_thesis: 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
let A, C be Subset of AS; ::_thesis: ( ( 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 implies d in C )
assume that
A1: ( A // C or C // A ) and
A2: ( a <> b & ( a,b // c,d or c,d // a,b ) ) and
A3: ( a in A & b in A ) and
A4: c in C ; ::_thesis: d in C
 A is being_line by A1, AFF_1:36;
then  a,b // A by A3, AFF_1:52;
then  c,d // A by A2, Th4;
then  c,d // C by A1, Th3;
hence  d in C by A4, Th2; ::_thesis: verum
end;

Lm2:  for AS being AffinSpace
for a, a9, d 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
let AS be AffinSpace; ::_thesis: for a, a9, d 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 )
let a, a9, d be Element of AS; ::_thesis: 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 )
let A, K be Subset of AS; ::_thesis: ( A // K & a in A & a9 in A & d in K implies ex d9 being Element of AS st
( d9 in K & a,d // a9,d9 ) )
assume that
A1: A // K and
A2: ( a in A & a9 in A ) and
A3: d in K ; ::_thesis: ex d9 being Element of AS st
( d9 in K & a,d // a9,d9 )
A4: A is being_line by A1, AFF_1:36;
now__::_thesis:_(_a_<>_a9_implies_ex_d9_being_Element_of_AS_st_
(_d9_in_K_&_a,d_//_a9,d9_)_)
assume A5: a <> a9 ; ::_thesis: ex d9 being Element of AS st
( d9 in K & a,d // a9,d9 )
consider d9 being Element of AS such that
A6: a,a9 // d,d9 and
A7: a,d // a9,d9 by DIRAF:40;
 d,d9 // a,a9 by A6, AFF_1:4;
then  d,d9 // A by A2, A4, A5, AFF_1:27;
then  d,d9 // K by A1, Th3;
then  d9 in K by A3, Th2;
hence  ex d9 being Element of AS st
( d9 in K & a,d // a9,d9 ) by A7; ::_thesis: verum
end;
hence  ex d9 being Element of AS st
( d9 in K & a,d // a9,d9 ) by A3, AFF_1:2; ::_thesis: verum
end;

theorem Th8: :: AFF_4:8
for AS being AffinSpace
for q, a, b, b9, a9 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
let AS be AffinSpace; ::_thesis: for q, a, b, b9, a9 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
let q, a, b, b9, a9 be Element of AS; ::_thesis: 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
let M, N be Subset of AS; ::_thesis: ( 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 implies q = b9 )
assume that
A1: q in M and
A2: q in N and
A3: a in M and
A4: b in N and
A5: b9 in N and
A6: q <> a and
A7: ( q <> b & M <> N ) and
A8: ( a,b // a9,b9 or b,a // b9,a9 ) and
A9: M is being_line and
A10: N is being_line and
A11: q = a9 ; ::_thesis: q = b9
A12: not LIN q,a,b
proof
assume  LIN q,a,b ; ::_thesis: contradiction
then consider A being Subset of AS such that
A13: ( A is being_line & q in A ) and
A14: a in A and
A15: b in A by AFF_1:21;
 M = A by A1, A3, A6, A9, A13, A14, AFF_1:18;
hence  contradiction by A2, A4, A7, A10, A13, A15, AFF_1:18; ::_thesis: verum
end;
 ( LIN q,b,b9 & a,b // a9,b9 ) by A2, A4, A5, A8, A10, AFF_1:4, AFF_1:21;
hence  q = b9 by A11, A12, AFF_1:55; ::_thesis: verum
end;

theorem Th9: :: AFF_4:9
for AS being AffinSpace
for q, a, a9, b, b9 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
let AS be AffinSpace; ::_thesis: for q, a, a9, b, b9 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
let q, a, a9, b, b9 be Element of AS; ::_thesis: 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
let M, N be Subset of AS; ::_thesis: ( 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 implies b = b9 )
assume that
A1: q in M and
A2: q in N and
A3: a in M and
A4: a9 in M and
A5: b in N and
A6: b9 in N and
A7: q <> a and
A8: ( q <> b & M <> N ) and
A9: ( a,b // a9,b9 or b,a // b9,a9 ) and
A10: M is being_line and
A11: N is being_line and
A12: a = a9 ; ::_thesis: b = b9
A13: ( a,b // a9,b & a,b // a9,b9 ) by A9, A12, AFF_1:2, AFF_1:4;
A14: not LIN q,a,b
proof
assume  LIN q,a,b ; ::_thesis: contradiction
then consider A being Subset of AS such that
A15: ( A is being_line & q in A ) and
A16: a in A and
A17: b in A by AFF_1:21;
 M = A by A1, A3, A7, A10, A15, A16, AFF_1:18;
hence  contradiction by A2, A5, A8, A11, A15, A17, AFF_1:18; ::_thesis: verum
end;
A18: LIN q,b,b by AFF_1:7;
 ( LIN q,a,a9 & LIN q,b,b9 ) by A1, A2, A3, A4, A5, A6, A10, A11, AFF_1:21;
hence  b = b9 by A14, A18, A13, AFF_1:56; ::_thesis: verum
end;

theorem Th10: :: AFF_4:10
for AS being AffinSpace
for a, b, b9, a9 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
let AS be AffinSpace; ::_thesis: for a, b, b9, a9 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
let a, b, b9, a9 be Element of AS; ::_thesis: 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
let M, N be Subset of AS; ::_thesis: ( ( 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 implies b = b9 )
assume that
A1: ( M // N or N // M ) and
A2: a in M and
A3: ( b in N & b9 in N ) and
A4: M <> N and
A5: ( ( a,b // a9,b9 or b,a // b9,a9 ) & a = a9 ) ; ::_thesis: b = b9
 a,b // a,b9 by A5, AFF_1:4;
then  LIN a,b,b9 by AFF_1:def_1;
then A6: LIN b,b9,a by AFF_1:6;
assume A7: b <> b9 ; ::_thesis: contradiction
 N is being_line by A1, AFF_1:36;
then  a in N by A3, A6, A7, AFF_1:25;
hence  contradiction by A1, A2, A4, AFF_1:45; ::_thesis: verum
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 )
proof
let AS be AffinSpace; ::_thesis: for a, b being Element of AS ex A being Subset of AS st
( a in A & b in A & A is being_line )
let a, b be Element of AS; ::_thesis: ex A being Subset of AS st
( a in A & b in A & A is being_line )
 LIN a,b,b by AFF_1:7;
then  ex A being Subset of AS st
( A is being_line & a in A & b in A & b in A ) by AFF_1:21;
hence  ex A being Subset of AS st
( a in A & b in A & A is being_line ) ; ::_thesis: verum
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
proof
let AS be AffinSpace; ::_thesis: for A being Subset of AS st A is being_line holds
ex q being Element of AS st not q in A
let A be Subset of AS; ::_thesis: ( A is being_line implies ex q being Element of AS st not q in A )
assume A1: A is being_line ; ::_thesis: not for q being Element of AS holds q in A
then consider a, b being Element of AS such that
A2: ( a in A & b in A ) and
A3: a <> b by AFF_1:19;
consider q being Element of AS such that
A4: not LIN a,b,q by A3, AFF_1:13;
 not q in A by A1, A2, A4, AFF_1:21;
hence  not for q being Element of AS holds q in A ; ::_thesis: verum
end;

definition
let AS be AffinSpace;
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 )  }  is Subset of AS
proof
set X =  {  a where a is Element of AS : ex b being Element of AS st
( a,b // K & b in P )  }  ;
now__::_thesis:_for_x_being_set_st_x_in__{__a_where_a_is_Element_of_AS_:_ex_b_being_Element_of_AS_st_
(_a,b_//_K_&_b_in_P_)__}__holds_
x_in_the_carrier_of_AS
let x be set ; ::_thesis: ( x in  {  a where a is Element of AS : ex b being Element of AS st
( a,b // K & b in P )  }  implies x in the carrier of AS )
assume  x in  {  a where a is Element of AS : ex b being Element of AS st
( a,b // K & b in P )  }  ; ::_thesis: x in the carrier of AS
then  ex a being Element of AS st
( a = x & ex b being Element of AS st
( a,b // K & b in P ) ) ;
hence  x in the carrier of AS ; ::_thesis: verum
end;
hence   {  a where a is Element of AS : ex b being Element of AS st
( a,b // K & b in P )  }  is Subset of AS by TARSKI:def_3; ::_thesis: verum
end;
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 )  }  ;

definition
let AS be AffinSpace;
let X be Subset of AS;
attrX is being_plane  means :Def2: :: 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) );
end;

:: deftheorem Def2 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) ) );

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
let AS be AffinSpace; ::_thesis: 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 ) )
let K, P be Subset of AS; ::_thesis: 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 ) )
let q be Element of AS; ::_thesis: ( q in Plane (K,P) iff ex b being Element of AS st
( q,b // K & b in P ) )
now__::_thesis:_(_q_in_Plane_(K,P)_implies_ex_b_being_Element_of_AS_st_
(_q,b_//_K_&_b_in_P_)_)
assume  q in Plane (K,P) ; ::_thesis: ex b being Element of AS st
( q,b // K & b in P )
then  ex a being Element of AS st
( a = q & ex b being Element of AS st
( a,b // K & b in P ) ) ;
hence  ex b being Element of AS st
( q,b // K & b in P ) ; ::_thesis: verum
end;
hence  ( q in Plane (K,P) iff ex b being Element of AS st
( q,b // K & b in P ) ) ; ::_thesis: verum
end;

theorem :: AFF_4:13
for AS being AffinSpace
for K, P being Subset of AS st not K is being_line holds
Plane (K,P) = {}
proof
let AS be AffinSpace; ::_thesis: for K, P being Subset of AS st not K is being_line holds
Plane (K,P) = {}
let K, P be Subset of AS; ::_thesis: ( not K is being_line implies Plane (K,P) = {} )
assume A1: not K is being_line ; ::_thesis: Plane (K,P) = {}
set x = the Element of Plane (K,P);
assume  Plane (K,P) <> {} ; ::_thesis: contradiction
then  the Element of Plane (K,P) in Plane (K,P) ;
then  ex a being Element of AS st
( the Element of Plane (K,P) = a & ex b being Element of AS st
( a,b // K & b in P ) ) ;
hence  contradiction by A1, AFF_1:26; ::_thesis: verum
end;

theorem Th14: :: AFF_4:14
for AS being AffinSpace
for K, P being Subset of AS st K is being_line holds
P c= Plane (K,P)
proof
let AS be AffinSpace; ::_thesis: for K, P being Subset of AS st K is being_line holds
P c= Plane (K,P)
let K, P be Subset of AS; ::_thesis: ( K is being_line implies P c= Plane (K,P) )
assume A1: K is being_line ; ::_thesis: P c= Plane (K,P)
now__::_thesis:_for_x_being_set_st_x_in_P_holds_
x_in_Plane_(K,P)
let x be set ; ::_thesis: ( x in P implies x in Plane (K,P) )
assume A2: x in P ; ::_thesis: x in Plane (K,P)
then reconsider a = x as Element of AS ;
 a,a // K by A1, AFF_1:33;
hence  x in Plane (K,P) by A2; ::_thesis: verum
end;
hence  P c= Plane (K,P) by TARSKI:def_3; ::_thesis: verum
end;

theorem :: AFF_4:15
for AS being AffinSpace
for K, P being Subset of AS st K // P holds
Plane (K,P) = P
proof
let AS be AffinSpace; ::_thesis: for K, P being Subset of AS st K // P holds
Plane (K,P) = P
let K, P be Subset of AS; ::_thesis: ( K // P implies Plane (K,P) = P )
set X = Plane (K,P);
assume A1: K // P ; ::_thesis: Plane (K,P) = P
then A2: P is being_line by AFF_1:36;
now__::_thesis:_for_x_being_set_st_x_in_Plane_(K,P)_holds_
x_in_P
let x be set ; ::_thesis: ( x in Plane (K,P) implies x in P )
assume  x in Plane (K,P) ; ::_thesis: x in P
then consider a being Element of AS such that
A3: x = a and
A4: ex b being Element of AS st
( a,b // K & b in P ) ;
consider b being Element of AS such that
A5: a,b // K and
A6: b in P by A4;
 a,b // P by A1, A5, AFF_1:43;
then  b,a // P by AFF_1:34;
hence  x in P by A2, A3, A6, AFF_1:23; ::_thesis: verum
end;
then A7: Plane (K,P) c= P by TARSKI:def_3;
 K is being_line by A1, AFF_1:36;
then  P c= Plane (K,P) by Th14;
hence  Plane (K,P) = P by A7, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem Th16: :: AFF_4:16
for AS being AffinSpace
for K, M, P being Subset of AS st K // M holds
Plane (K,P) = Plane (M,P)
proof
let AS be AffinSpace; ::_thesis: for K, M, P being Subset of AS st K // M holds
Plane (K,P) = Plane (M,P)
let K, M, P be Subset of AS; ::_thesis: ( K // M implies Plane (K,P) = Plane (M,P) )
assume A1: K // M ; ::_thesis: Plane (K,P) = Plane (M,P)
now__::_thesis:_for_x_being_set_holds_
(_x_in_Plane_(K,P)_iff_x_in_Plane_(M,P)_)
let x be set ; ::_thesis: ( x in Plane (K,P) iff x in Plane (M,P) )
A2: now__::_thesis:_(_x_in_Plane_(M,P)_implies_x_in_Plane_(K,P)_)
assume  x in Plane (M,P) ; ::_thesis: x in Plane (K,P)
then consider a being Element of AS such that
A3: x = a and
A4: ex b being Element of AS st
( a,b // M & b in P ) ;
consider b being Element of AS such that
A5: a,b // M and
A6: b in P by A4;
 a,b // K by A1, A5, AFF_1:43;
hence  x in Plane (K,P) by A3, A6; ::_thesis: verum
end;
now__::_thesis:_(_x_in_Plane_(K,P)_implies_x_in_Plane_(M,P)_)
assume  x in Plane (K,P) ; ::_thesis: x in Plane (M,P)
then consider a being Element of AS such that
A7: x = a and
A8: ex b being Element of AS st
( a,b // K & b in P ) ;
consider b being Element of AS such that
A9: a,b // K and
A10: b in P by A8;
 a,b // M by A1, A9, AFF_1:43;
hence  x in Plane (M,P) by A7, A10; ::_thesis: verum
end;
hence  ( x in Plane (K,P) iff x in Plane (M,P) ) by A2; ::_thesis: verum
end;
hence  Plane (K,P) = Plane (M,P) by TARSKI:1; ::_thesis: verum
end;

theorem :: AFF_4:17
for AS being AffinSpace
for p, a, b, a9, b9 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
let AS be AffinSpace; ::_thesis: for p, a, b, a9, b9 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 )
let p, a, b, a9, b9 be Element of AS; ::_thesis: 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 )
let M, N, P, Q be Subset of AS; ::_thesis: ( 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 implies ex q being Element of AS st
( q in P & q in Q ) )
assume that
A1: p in M and
A2: a in M and
A3: b in M and
A4: p in N and
A5: a9 in N and
A6: b9 in N and
A7: not p in P and
A8: not p in Q and
A9: M <> N and
A10: a in P and
A11: a9 in P and
A12: b in Q and
A13: b9 in Q and
A14: M is being_line and
A15: N is being_line and
A16: P is being_line and
A17: Q is being_line ; ::_thesis: ( P // Q or ex q being Element of AS st
( q in P & q in Q ) )
A18: a <> a9 by A1, A2, A4, A5, A7, A9, A10, A14, A15, AFF_1:18;
 LIN p,a,b by A1, A2, A3, A14, AFF_1:21;
then consider c being Element of AS such that
A19: LIN p,a9,c and
A20: a,a9 // b,c by A7, A10, Th1;
set D = Line (b,c);
A21: b in Line (b,c) by AFF_1:15;
A22: c in Line (b,c) by AFF_1:15;
A23: b <> b9 by A1, A3, A4, A6, A8, A9, A12, A14, A15, AFF_1:18;
A24: c in N by A4, A5, A7, A11, A15, A19, AFF_1:25;
then A25: b <> c by A1, A3, A4, A8, A9, A12, A14, A15, AFF_1:18;
then A26: Line (b,c) is being_line by AFF_1:def_3;
now__::_thesis:_(_Line_(b,c)_<>_Q_implies_ex_q_being_Element_of_AS_st_
(_q_in_P_&_q_in_Q_)_)
assume  Line (b,c) <> Q ; ::_thesis: ex q being Element of AS st
( q in P & q in Q )
then A27: c <> b9 by A12, A13, A17, A23, A26, A21, A22, AFF_1:18;
 LIN b9,c,a9 by A5, A6, A15, A24, AFF_1:21;
then consider q being Element of AS such that
A28: LIN b9,b,q and
A29: c,b // a9,q by A27, Th1;
 a9,a // c,b by A20, AFF_1:4;
then  a9,a // a9,q by A25, A29, AFF_1:5;
then  LIN a9,a,q by AFF_1:def_1;
then A30: q in P by A10, A11, A16, A18, AFF_1:25;
 q in Q by A12, A13, A17, A23, A28, AFF_1:25;
hence  ex q being Element of AS st
( q in P & q in Q ) by A30; ::_thesis: verum
end;
hence  ( P // Q or ex q being Element of AS st
( q in P & q in Q ) ) by A10, A11, A12, A16, A17, A18, A20, A25, A22, AFF_1:38; ::_thesis: verum
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 )
proof
let AS be AffinSpace; ::_thesis: 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 )
let a, b, a9, b9 be Element of AS; ::_thesis: 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 )
let M, N, P, Q be Subset of AS; ::_thesis: ( 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 implies ex q being Element of AS st
( q in P & q in Q ) )
assume that
A1: a in M and
A2: b in M and
A3: a9 in N and
A4: b9 in N and
A5: a in P and
A6: a9 in P and
A7: b in Q and
A8: b9 in Q and
A9: M <> N and
A10: M // N and
A11: P is being_line and
A12: Q is being_line ; ::_thesis: ( P // Q or ex q being Element of AS st
( q in P & q in Q ) )
A13: a <> a9 by A1, A3, A9, A10, AFF_1:45;
A14: N is being_line by A10, AFF_1:36;
A15: b <> b9 by A2, A4, A9, A10, AFF_1:45;
A16: M is being_line by A10, AFF_1:36;
now__::_thesis:_(_a_<>_b_&_not_P_//_Q_implies_ex_q_being_Element_of_AS_st_
(_q_in_P_&_q_in_Q_)_)
assume A17: a <> b ; ::_thesis: ( P // Q or ex q being Element of AS st
( q in P & q in Q ) )
consider c being Element of AS such that
A18: a,b // a9,c and
A19: a,a9 // b,c by DIRAF:40;
set D = Line (b,c);
A20: b in Line (b,c) by AFF_1:15;
A21: c in Line (b,c) by AFF_1:15;
 a,b // N by A1, A2, A10, A16, AFF_1:43, AFF_1:52;
then  a9,c // N by A17, A18, AFF_1:32;
then A22: c in N by A3, A14, AFF_1:23;
then A23: b <> c by A2, A9, A10, AFF_1:45;
then A24: Line (b,c) is being_line by AFF_1:def_3;
now__::_thesis:_(_Line_(b,c)_<>_Q_implies_ex_q_being_Element_of_AS_st_
(_q_in_P_&_q_in_Q_)_)
assume  Line (b,c) <> Q ; ::_thesis: ex q being Element of AS st
( q in P & q in Q )
then A25: c <> b9 by A7, A8, A12, A15, A24, A20, A21, AFF_1:18;
 LIN b9,c,a9 by A3, A4, A14, A22, AFF_1:21;
then consider q being Element of AS such that
A26: LIN b9,b,q and
A27: c,b // a9,q by A25, Th1;
 a9,a // c,b by A19, AFF_1:4;
then  a9,a // a9,q by A23, A27, AFF_1:5;
then  LIN a9,a,q by AFF_1:def_1;
then A28: q in P by A5, A6, A11, A13, AFF_1:25;
 q in Q by A7, A8, A12, A15, A26, AFF_1:25;
hence  ex q being Element of AS st
( q in P & q in Q ) by A28; ::_thesis: verum
end;
hence  ( P // Q or ex q being Element of AS st
( q in P & q in Q ) ) by A5, A6, A7, A11, A12, A13, A19, A23, A21, AFF_1:38; ::_thesis: verum
end;
hence  ( P // Q or ex q being Element of AS st
( q in P & q in Q ) ) by A5, A7; ::_thesis: verum
end;

Lm4:  for AS being AffinSpace
for a being Element of AS
for Q, K, P being Subset of AS st a in Q & a in Plane (K,P) & K // Q holds
Q c= Plane (K,P)
proof
let AS be AffinSpace; ::_thesis: for a being Element of AS
for Q, K, P being Subset of AS st a in Q & a in Plane (K,P) & K // Q holds
Q c= Plane (K,P)
let a be Element of AS; ::_thesis: for Q, K, P being Subset of AS st a in Q & a in Plane (K,P) & K // Q holds
Q c= Plane (K,P)
let Q, K, P be Subset of AS; ::_thesis: ( a in Q & a in Plane (K,P) & K // Q implies Q c= Plane (K,P) )
assume that
A1: a in Q and
A2: a in Plane (K,P) and
A3: K // Q ; ::_thesis: Q c= Plane (K,P)
now__::_thesis:_for_x_being_set_st_x_in_Q_holds_
x_in_Plane_(K,P)
A4: Plane (K,P) = Plane (Q,P) by A3, Th16;
let x be set ; ::_thesis: ( x in Q implies x in Plane (K,P) )
assume A5: x in Q ; ::_thesis: x in Plane (K,P)
reconsider c = x as Element of AS by A5;
A6: Q is being_line by A3, AFF_1:36;
consider b being Element of AS such that
A7: a,b // K and
A8: b in P by A2, Lm3;
 a,b // Q by A3, A7, AFF_1:43;
then  b in Q by A1, A6, AFF_1:23;
then  c,b // Q by A5, A6, AFF_1:23;
hence  x in Plane (K,P) by A8, A4; ::_thesis: verum
end;
hence  Q c= Plane (K,P) by TARSKI:def_3; ::_thesis: verum
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
let AS be AffinSpace; ::_thesis: 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)
let a, b be Element of AS; ::_thesis: 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)
let K, P, Q be Subset of AS; ::_thesis: ( 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 implies Q c= Plane (K,P) )
assume that
A1: K is being_line and
A2: P is being_line and
A3: Q is being_line and
A4: a in Plane (K,P) and
A5: b in Plane (K,P) and
A6: a <> b and
A7: a in Q and
A8: b in Q ; ::_thesis: Q c= Plane (K,P)
now__::_thesis:_for_x_being_set_st_x_in_Q_holds_
x_in_Plane_(K,P)
let x be set ; ::_thesis: ( x in Q implies x in Plane (K,P) )
assume A9: x in Q ; ::_thesis: x in Plane (K,P)
then reconsider c = x as Element of AS ;
consider a9 being Element of AS such that
A10: a,a9 // K and
A11: a9 in P by A4, Lm3;
consider Y being Subset of AS such that
A12: b in Y and
A13: K // Y by A1, AFF_1:49;
consider X being Subset of AS such that
A14: a in X and
A15: K // X by A1, AFF_1:49;
consider b9 being Element of AS such that
A16: b,b9 // K and
A17: b9 in P by A5, Lm3;
 b,b9 // Y by A16, A13, AFF_1:43;
then A18: b9 in Y by A12, Th2;
 a,a9 // X by A10, A15, AFF_1:43;
then A19: a9 in X by A14, Th2;
A20: X // Y by A15, A13, AFF_1:44;
A21: now__::_thesis:_(_X_<>_Y_implies_x_in_Plane_(K,P)_)
A22: now__::_thesis:_(_ex_q_being_Element_of_AS_st_
(_q_in_P_&_q_in_Q_&_not_P_//_Q_)_implies_x_in_Plane_(K,P)_)
given q being Element of AS such that A23: q in P and
A24: q in Q and
A25: not P // Q ; ::_thesis: x in Plane (K,P)
A26: P <> Q by A2, A25, AFF_1:41;
A27: now__::_thesis:_(_q_<>_b_implies_x_in_Plane_(K,P)_)
assume A28: q <> b ; ::_thesis: x in Plane (K,P)
then A29: b <> b9 by A2, A3, A8, A17, A23, A24, A26, AFF_1:18;
A30: now__::_thesis:_(_q_<>_b9_implies_x_in_Plane_(K,P)_)
A31: q,b9 // P by A2, A17, A23, AFF_1:23;
 LIN q,b,c by A3, A8, A9, A24, AFF_1:21;
then consider c9 being Element of AS such that
A32: LIN q,b9,c9 and
A33: b,b9 // c,c9 by A28, Th1;
assume A34: q <> b9 ; ::_thesis: x in Plane (K,P)
 q,b9 // q,c9 by A32, AFF_1:def_1;
then  q,c9 // P by A34, A31, AFF_1:32;
then A35: c9 in P by A23, Th2;
 c,c9 // K by A16, A29, A33, AFF_1:32;
hence  x in Plane (K,P) by A35; ::_thesis: verum
end;
now__::_thesis:_(_q_=_b9_implies_x_in_Plane_(K,P)_)
assume A36: q = b9 ; ::_thesis: x in Plane (K,P)
 b,q // Q by A3, A8, A24, AFF_1:23;
then  Q c= Plane (K,P) by A4, A7, A16, A28, A36, Lm4, AFF_1:53;
hence  x in Plane (K,P) by A9; ::_thesis: verum
end;
hence  x in Plane (K,P) by A30; ::_thesis: verum
end;
now__::_thesis:_(_q_<>_a_implies_x_in_Plane_(K,P)_)
assume A37: q <> a ; ::_thesis: x in Plane (K,P)
then A38: a <> a9 by A2, A3, A7, A11, A23, A24, A26, AFF_1:18;
A39: now__::_thesis:_(_q_<>_a9_implies_x_in_Plane_(K,P)_)
A40: q,a9 // P by A2, A11, A23, AFF_1:23;
 LIN q,a,c by A3, A7, A9, A24, AFF_1:21;
then consider c9 being Element of AS such that
A41: LIN q,a9,c9 and
A42: a,a9 // c,c9 by A37, Th1;
assume A43: q <> a9 ; ::_thesis: x in Plane (K,P)
 q,a9 // q,c9 by A41, AFF_1:def_1;
then  q,c9 // P by A43, A40, AFF_1:32;
then A44: c9 in P by A23, Th2;
 c,c9 // K by A10, A38, A42, AFF_1:32;
hence  x in Plane (K,P) by A44; ::_thesis: verum
end;
now__::_thesis:_(_q_=_a9_implies_x_in_Plane_(K,P)_)
assume A45: q = a9 ; ::_thesis: x in Plane (K,P)
 a,q // Q by A3, A7, A24, AFF_1:23;
then  Q c= Plane (K,P) by A4, A7, A10, A37, A45, Lm4, AFF_1:53;
hence  x in Plane (K,P) by A9; ::_thesis: verum
end;
hence  x in Plane (K,P) by A39; ::_thesis: verum
end;
hence  x in Plane (K,P) by A6, A27; ::_thesis: verum
end;
A46: now__::_thesis:_(_P_//_Q_implies_x_in_Plane_(K,P)_)
assume A47: P // Q ; ::_thesis: x in Plane (K,P)
A48: now__::_thesis:_(_P_<>_Q_implies_x_in_Plane_(K,P)_)
assume  P <> Q ; ::_thesis: x in Plane (K,P)
then A49: b <> b9 by A8, A17, A47, AFF_1:45;
now__::_thesis:_(_c_<>_b_implies_x_in_Plane_(K,P)_)
assume A50: c <> b ; ::_thesis: x in Plane (K,P)
consider c9 being Element of AS such that
A51: b,c // b9,c9 and
A52: b,b9 // c,c9 by DIRAF:40;
 b,c // Q by A3, A8, A9, AFF_1:23;
then  b9,c9 // Q by A50, A51, AFF_1:32;
then  b9,c9 // P by A47, AFF_1:43;
then A53: c9 in P by A17, Th2;
 c,c9 // K by A16, A49, A52, AFF_1:32;
hence  x in Plane (K,P) by A53; ::_thesis: verum
end;
hence  x in Plane (K,P) by A5; ::_thesis: verum
end;
now__::_thesis:_(_P_=_Q_implies_x_in_Plane_(K,P)_)
assume A54: P = Q ; ::_thesis: x in Plane (K,P)
 c,c // K by A1, AFF_1:33;
hence  x in Plane (K,P) by A9, A54; ::_thesis: verum
end;
hence  x in Plane (K,P) by A48; ::_thesis: verum
end;
assume  X <> Y ; ::_thesis: x in Plane (K,P)
then  ( P // Q or ex q being Element of AS st
( q in P & q in Q ) ) by A2, A3, A7, A8, A11, A17, A14, A12, A20, A19, A18, Th18;
hence  x in Plane (K,P) by A46, A22; ::_thesis: verum
end;
A55: X is being_line by A10, A15, AFF_1:26, AFF_1:43;
now__::_thesis:_(_X_=_Y_implies_x_in_Plane_(K,P)_)
assume  X = Y ; ::_thesis: x in Plane (K,P)
then  Q = X by A3, A6, A7, A8, A14, A12, A55, AFF_1:18;
then  Q c= Plane (K,P) by A4, A7, A15, Lm4;
hence  x in Plane (K,P) by A9; ::_thesis: verum
end;
hence  x in Plane (K,P) by A21; ::_thesis: verum
end;
hence  Q c= Plane (K,P) by TARSKI:def_3; ::_thesis: verum
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
proof
let AS be AffinSpace; ::_thesis: 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
let a, b be Element of AS; ::_thesis: 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
let X be Subset of AS; ::_thesis: ( X is being_plane & a in X & b in X & a <> b implies Line (a,b) c= X )
assume that
A1: X is being_plane and
A2: ( a in X & b in X ) and
A3: a <> b ; ::_thesis: Line (a,b) c= X
set Q = Line (a,b);
A4: ( a in Line (a,b) & b in Line (a,b) ) by AFF_1:15;
 ( Line (a,b) is being_line & ex K, P being Subset of AS st
( K is being_line & P is being_line & not K // P & X = Plane (K,P) ) ) by A1, A3, Def2, AFF_1:def_3;
hence  Line (a,b) c= X by A2, A3, A4, Lm5; ::_thesis: verum
end;

Lm6:  for AS being AffinSpace
for K, Q, P being Subset of AS st K is being_line & Q c= Plane (K,P) holds
Plane (K,Q) c= Plane (K,P)
proof
let AS be AffinSpace; ::_thesis: for K, Q, P being Subset of AS st K is being_line & Q c= Plane (K,P) holds
Plane (K,Q) c= Plane (K,P)
let K, Q, P be Subset of AS; ::_thesis: ( K is being_line & Q c= Plane (K,P) implies Plane (K,Q) c= Plane (K,P) )
assume that
A1: K is being_line and
A2: Q c= Plane (K,P) ; ::_thesis: Plane (K,Q) c= Plane (K,P)
now__::_thesis:_for_x_being_set_st_x_in_Plane_(K,Q)_holds_
x_in_Plane_(K,P)
let x be set ; ::_thesis: ( x in Plane (K,Q) implies x in Plane (K,P) )
assume  x in Plane (K,Q) ; ::_thesis: x in Plane (K,P)
then consider a being Element of AS such that
A3: x = a and
A4: ex b being Element of AS st
( a,b // K & b in Q ) ;
consider b being Element of AS such that
A5: a,b // K and
A6: b in Q by A4;
consider c being Element of AS such that
A7: b,c // K and
A8: c in P by A2, A6, Lm3;
consider M being Subset of AS such that
A9: b in M and
A10: K // M by A1, AFF_1:49;
 a,b // M by A5, A10, AFF_1:43;
then A11: a in M by A9, Th2;
 b,c // M by A7, A10, AFF_1:43;
then  c in M by A9, Th2;
then  a,c // K by A10, A11, AFF_1:40;
hence  x in Plane (K,P) by A3, A8; ::_thesis: verum
end;
hence  Plane (K,Q) c= Plane (K,P) by TARSKI:def_3; ::_thesis: verum
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)
proof
let AS be AffinSpace; ::_thesis: 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)
let K, P, Q be Subset of AS; ::_thesis: ( K is being_line & P is being_line & Q is being_line & not K // Q & Q c= Plane (K,P) implies Plane (K,Q) = Plane (K,P) )
assume that
A1: K is being_line and
A2: P is being_line and
A3: Q is being_line and
A4: not K // Q and
A5: Q c= Plane (K,P) ; ::_thesis: Plane (K,Q) = Plane (K,P)
A6: Plane (K,Q) c= Plane (K,P) by A1, A5, Lm6;
consider a, b being Element of AS such that
A7: a in Q and
A8: b in Q and
A9: a <> b by A3, AFF_1:19;
consider b9 being Element of AS such that
A10: b,b9 // K and
A11: b9 in P by A5, A8, Lm3;
 b9,b // K by A10, AFF_1:34;
then A12: b9 in Plane (K,Q) by A8;
consider a9 being Element of AS such that
A13: a,a9 // K and
A14: a9 in P by A5, A7, Lm3;
A15: a9 <> b9
proof
consider A being Subset of AS such that
A16: a9 in A and
A17: K // A by A1, AFF_1:49;
 a9,a // A by A13, A17, Th3;
then A18: a in A by A16, Th2;
assume  a9 = b9 ; ::_thesis: contradiction
then  a9,b // A by A10, A17, Th3;
then A19: b in A by A16, Th2;
 A is being_line by A17, AFF_1:36;
hence  contradiction by A3, A4, A7, A8, A9, A17, A19, A18, AFF_1:18; ::_thesis: verum
end;
 a9,a // K by A13, AFF_1:34;
then  a9 in Plane (K,Q) by A7;
then  Plane (K,P) c= Plane (K,Q) by A1, A2, A3, A14, A11, A15, A12, Lm5, Lm6;
hence  Plane (K,Q) = Plane (K,P) by A6, XBOOLE_0:def_10; ::_thesis: verum
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 )
proof
let AS be AffinSpace; ::_thesis: 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 )
let K, P, Q be Subset of AS; ::_thesis: ( K is being_line & P is being_line & Q is being_line & Q c= Plane (K,P) & not P // Q implies ex q being Element of AS st
( q in P & q in Q ) )
assume that
A1: K is being_line and
A2: P is being_line and
A3: Q is being_line and
A4: Q c= Plane (K,P) ; ::_thesis: ( P // Q or ex q being Element of AS st
( q in P & q in Q ) )
consider a, b being Element of AS such that
A5: a in Q and
A6: b in Q and
A7: a <> b by A3, AFF_1:19;
consider a9 being Element of AS such that
A8: a,a9 // K and
A9: a9 in P by A4, A5, Lm3;
consider A being Subset of AS such that
A10: a9 in A and
A11: K // A by A1, AFF_1:49;
A12: a9,a // A by A8, A11, Th3;
then A13: a in A by A10, Th2;
consider b9 being Element of AS such that
A14: b,b9 // K and
A15: b9 in P by A4, A6, Lm3;
consider M being Subset of AS such that
A16: b9 in M and
A17: K // M by A1, AFF_1:49;
A18: b9,b // M by A14, A17, Th3;
then A19: b in M by A16, Th2;
A20: A is being_line by A11, AFF_1:36;
A21: now__::_thesis:_(_A_=_M_implies_ex_q_being_Element_of_AS_st_
(_q_in_P_&_q_in_Q_)_)
assume  A = M ; ::_thesis: ex q being Element of AS st
( q in P & q in Q )
then A22: b in A by A16, A18, Th2;
 a in A by A10, A12, Th2;
then  a9 in Q by A3, A5, A6, A7, A10, A20, A22, AFF_1:18;
hence  ex q being Element of AS st
( q in P & q in Q ) by A9; ::_thesis: verum
end;
 A // M by A11, A17, AFF_1:44;
hence  ( P // Q or ex q being Element of AS st
( q in P & q in Q ) ) by A2, A3, A5, A6, A9, A15, A10, A16, A13, A19, A21, Th18; ::_thesis: verum
end;

theorem Th22: :: AFF_4:22
for AS being AffinSpace
for X, M, N 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
let AS be AffinSpace; ::_thesis: for X, M, N 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 )
let X, M, N be Subset of AS; ::_thesis: ( X is being_plane & M is being_line & N is being_line & M c= X & N c= X & not M // N implies ex q being Element of AS st
( q in M & q in N ) )
assume that
A1: X is being_plane and
A2: M is being_line and
A3: N is being_line and
A4: ( M c= X & N c= X ) ; ::_thesis: ( M // N or ex q being Element of AS st
( q in M & q in N ) )
consider K, P being Subset of AS such that
A5: K is being_line and
A6: P is being_line and
 not K // P and
A7: X = Plane (K,P) by A1, Def2;
A8: now__::_thesis:_(_not_K_//_N_&_not_M_//_N_implies_ex_q_being_Element_of_AS_st_
(_q_in_M_&_q_in_N_)_)
assume  not K // N ; ::_thesis: ( M // N or ex q being Element of AS st
( q in M & q in N ) )
then  M c= Plane (K,N) by A3, A4, A5, A6, A7, Th20;
then  ( N // M or ex q being Element of AS st
( q in N & q in M ) ) by A2, A3, A5, Th21;
hence  ( M // N or ex q being Element of AS st
( q in M & q in N ) ) ; ::_thesis: verum
end;
now__::_thesis:_(_not_K_//_M_&_not_M_//_N_implies_ex_q_being_Element_of_AS_st_
(_q_in_M_&_q_in_N_)_)
assume  not K // M ; ::_thesis: ( M // N or ex q being Element of AS st
( q in M & q in N ) )
then  N c= Plane (K,M) by A2, A4, A5, A6, A7, Th20;
hence  ( M // N or ex q being Element of AS st
( q in M & q in N ) ) by A2, A3, A5, Th21; ::_thesis: verum
end;
hence  ( M // N or ex q being Element of AS st
( q in M & q in N ) ) by A8, AFF_1:44; ::_thesis: verum
end;

theorem Th23: :: AFF_4:23
for AS being AffinSpace
for a being Element of AS
for X, M, N 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
let AS be AffinSpace; ::_thesis: for a being Element of AS
for X, M, N 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
let a be Element of AS; ::_thesis: for X, M, N 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
let X, M, N be Subset of AS; ::_thesis: ( X is being_plane & a in X & M c= X & a in N & ( M // N or N // M ) implies N c= X )
assume that
A1: X is being_plane and
A2: a in X and
A3: M c= X and
A4: a in N and
A5: ( M // N or N // M ) ; ::_thesis: N c= X
A6: M is being_line by A5, AFF_1:36;
consider K, P being Subset of AS such that
A7: K is being_line and
A8: P is being_line and
 not K // P and
A9: X = Plane (K,P) by A1, Def2;
A10: N is being_line by A5, AFF_1:36;
A11: now__::_thesis:_(_not_K_//_M_implies_N_c=_X_)
assume A12: not K // M ; ::_thesis: N c= X
then A13: X = Plane (K,M) by A3, A6, A7, A8, A9, Th20;
A14: a in Plane (K,M) by A2, A3, A6, A7, A8, A9, A12, Th20;
now__::_thesis:_(_M_<>_N_implies_N_c=_X_)
consider a9 being Element of AS such that
A15: a,a9 // K and
A16: a9 in M by A14, Lm3;
consider b9 being Element of AS such that
A17: a9 <> b9 and
A18: b9 in M by A6, AFF_1:20;
consider b being Element of AS such that
A19: a9,a // b9,b and
A20: a9,b9 // a,b by DIRAF:40;
assume A21: M <> N ; ::_thesis: N c= X
then  a <> a9 by A4, A5, A16, AFF_1:45;
then  b,b9 // K by A15, A19, Th4;
then A22: b in Plane (K,M) by A18;
A23: a <> b
proof
assume  a = b ; ::_thesis: contradiction
then  a,a9 // a,b9 by A19, AFF_1:4;
then  LIN a,a9,b9 by AFF_1:def_1;
then  LIN a9,b9,a by AFF_1:6;
then  a in M by A6, A16, A17, A18, AFF_1:25;
hence  contradiction by A4, A5, A21, AFF_1:45; ::_thesis: verum
end;
 a,b // M by A6, A16, A17, A18, A20, AFF_1:32, AFF_1:52;
then  a,b // N by A5, Th3;
then  b in N by A4, Th2;
hence  N c= X by A2, A4, A6, A10, A7, A13, A23, A22, Lm5; ::_thesis: verum
end;
hence  N c= X by A3; ::_thesis: verum
end;
now__::_thesis:_(_K_//_M_implies_N_c=_X_)
assume  K // M ; ::_thesis: N c= X
then  K // N by A5, AFF_1:44;
hence  N c= X by A2, A4, A9, Lm4; ::_thesis: verum
end;
hence  N c= X by A11; ::_thesis: verum
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
proof
let AS be AffinSpace; ::_thesis: 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
let a, b be Element of AS; ::_thesis: 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
let X, Y be Subset of AS; ::_thesis: ( X is being_plane & Y is being_plane & a in X & b in X & a in Y & b in Y & X <> Y & a <> b implies X /\ Y is being_line )
assume that
A1: X is being_plane and
A2: Y is being_plane and
A3: ( a in X & b in X ) and
A4: ( a in Y & b in Y ) and
A5: X <> Y and
A6: a <> b ; ::_thesis: X /\ Y is being_line
set Z = X /\ Y;
set Q = Line (a,b);
A7: Line (a,b) c= X by A1, A3, A6, Th19;
A8: Line (a,b) c= Y by A2, A4, A6, Th19;
A9: Line (a,b) is being_line by A6, AFF_1:def_3;
A10: X /\ Y c= Line (a,b)
proof
assume  not X /\ Y c= Line (a,b) ; ::_thesis: contradiction
then consider x being set  such that
A11: x in X /\ Y and
A12: not x in Line (a,b) by TARSKI:def_3;
reconsider a9 = x as Element of AS by A11;
A13: x in Y by A11, XBOOLE_0:def_4;
A14: x in X by A11, XBOOLE_0:def_4;
 for y being set holds
( y in X iff y in Y )
proof
let y be set ; ::_thesis: ( y in X iff y in Y )
A15: now__::_thesis:_(_y_in_Y_implies_y_in_X_)
assume A16: y in Y ; ::_thesis: y in X
now__::_thesis:_(_y_<>_x_implies_y_in_X_)
reconsider b9 = y as Element of AS by A16;
set M = Line (a9,b9);
A17: a9 in Line (a9,b9) by AFF_1:15;
A18: b9 in Line (a9,b9) by AFF_1:15;
assume A19: y <> x ; ::_thesis: y in X
then A20: Line (a9,b9) is being_line by AFF_1:def_3;
A21: Line (a9,b9) c= Y by A2, A13, A16, A19, Th19;
A22: now__::_thesis:_(_not_Line_(a9,b9)_//_Line_(a,b)_implies_y_in_X_)
assume  not Line (a9,b9) // Line (a,b) ; ::_thesis: y in X
then consider q being Element of AS such that
A23: q in Line (a9,b9) and
A24: q in Line (a,b) by A2, A9, A8, A20, A21, Th22;
 Line (a9,b9) = Line (a9,q) by A12, A20, A17, A23, A24, AFF_1:57;
then  Line (a9,b9) c= X by A1, A7, A12, A14, A24, Th19;
hence  y in X by A18; ::_thesis: verum
end;
now__::_thesis:_(_Line_(a9,b9)_//_Line_(a,b)_implies_y_in_X_)
assume  Line (a9,b9) // Line (a,b) ; ::_thesis: y in X
then  Line (a9,b9) c= X by A1, A7, A14, A17, Th23;
hence  y in X by A18; ::_thesis: verum
end;
hence  y in X by A22; ::_thesis: verum
end;
hence  y in X by A11, XBOOLE_0:def_4; ::_thesis: verum
end;
now__::_thesis:_(_y_in_X_implies_y_in_Y_)
assume A25: y in X ; ::_thesis: y in Y
now__::_thesis:_(_y_<>_x_implies_y_in_Y_)
reconsider b9 = y as Element of AS by A25;
set M = Line (a9,b9);
A26: a9 in Line (a9,b9) by AFF_1:15;
A27: b9 in Line (a9,b9) by AFF_1:15;
assume A28: y <> x ; ::_thesis: y in Y
then A29: Line (a9,b9) is being_line by AFF_1:def_3;
A30: Line (a9,b9) c= X by A1, A14, A25, A28, Th19;
A31: now__::_thesis:_(_not_Line_(a9,b9)_//_Line_(a,b)_implies_y_in_Y_)
assume  not Line (a9,b9) // Line (a,b) ; ::_thesis: y in Y
then consider q being Element of AS such that
A32: q in Line (a9,b9) and
A33: q in Line (a,b) by A1, A9, A7, A29, A30, Th22;
 Line (a9,b9) = Line (a9,q) by A12, A29, A26, A32, A33, AFF_1:57;
then  Line (a9,b9) c= Y by A2, A8, A12, A13, A33, Th19;
hence  y in Y by A27; ::_thesis: verum
end;
now__::_thesis:_(_Line_(a9,b9)_//_Line_(a,b)_implies_y_in_Y_)
assume  Line (a9,b9) // Line (a,b) ; ::_thesis: y in Y
then  Line (a9,b9) c= Y by A2, A8, A13, A26, Th23;
hence  y in Y by A27; ::_thesis: verum
end;
hence  y in Y by A31; ::_thesis: verum
end;
hence  y in Y by A11, XBOOLE_0:def_4; ::_thesis: verum
end;
hence  ( y in X iff y in Y ) by A15; ::_thesis: verum
end;
hence  contradiction by A5, TARSKI:1; ::_thesis: verum
end;
 Line (a,b) c= X /\ Y by A7, A8, XBOOLE_1:19;
hence  X /\ Y is being_line by A9, A10, XBOOLE_0:def_10; ::_thesis: verum
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
proof
let AS be AffinSpace; ::_thesis: 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
let a, b, c be Element of AS; ::_thesis: 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
let X, Y be Subset of AS; ::_thesis: ( 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 implies X = Y )
assume that
A1: ( X is being_plane & Y is being_plane ) and
A2: ( a in X & b in X ) and
A3: c in X and
A4: ( a in Y & b in Y ) and
A5: c in Y and
A6: not LIN a,b,c ; ::_thesis: X = Y
assume A7: not X = Y ; ::_thesis: contradiction
 a <> b by A6, AFF_1:7;
then A8: X /\ Y is being_line by A1, A2, A4, A7, Th24;
A9: c in X /\ Y by A3, A5, XBOOLE_0:def_4;
 ( a in X /\ Y & b in X /\ Y ) by A2, A4, XBOOLE_0:def_4;
hence  contradiction by A6, A8, A9, AFF_1:21; ::_thesis: verum
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
let AS be AffinSpace; ::_thesis: 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
let a, b, c be Element of AS; ::_thesis: 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
let M be Subset of AS; ::_thesis: ( M is being_line & a in M & b in M & a <> b & not c in M implies not LIN a,b,c )
assume A1: ( M is being_line & a in M & b in M & a <> b & not c in M ) ; ::_thesis: not LIN a,b,c
assume  LIN a,b,c ; ::_thesis: contradiction
then  ex N being Subset of AS st
( N is being_line & a in N & b in N & c in N ) by AFF_1:21;
hence  contradiction by A1, AFF_1:18; ::_thesis: verum
end;

theorem Th26: :: AFF_4:26
for AS being AffinSpace
for X, Y, M, N 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
let AS be AffinSpace; ::_thesis: for X, Y, M, N 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
let X, Y, M, N be Subset of AS; ::_thesis: ( 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 implies X = Y )
assume that
A1: X is being_plane and
A2: Y is being_plane and
A3: M is being_line and
A4: N is being_line and
A5: ( M c= X & N c= X ) and
A6: ( M c= Y & N c= Y ) and
A7: M <> N ; ::_thesis: X = Y
consider a, b being Element of AS such that
A8: a in M and
A9: b in M and
A10: a <> b by A3, AFF_1:19;
A11: now__::_thesis:_(_ex_q_being_Element_of_AS_st_
(_q_in_M_&_q_in_N_)_implies_X_=_Y_)
given q being Element of AS such that A12: q in M and
A13: q in N ; ::_thesis: X = Y
consider p being Element of AS such that
A14: q <> p and
A15: p in N by A4, AFF_1:20;
A16: not p in M by A3, A4, A7, A12, A13, A14, A15, AFF_1:18;
A17: now__::_thesis:_(_b_<>_q_implies_X_=_Y_)
assume  b <> q ; ::_thesis: X = Y
then  not LIN b,q,p by A3, A9, A12, A16, Lm7;
hence  X = Y by A1, A2, A5, A6, A9, A12, A15, Th25; ::_thesis: verum
end;
now__::_thesis:_(_a_<>_q_implies_X_=_Y_)
assume  a <> q ; ::_thesis: X = Y
then  not LIN a,q,p by A3, A8, A12, A16, Lm7;
hence  X = Y by A1, A2, A5, A6, A8, A12, A15, Th25; ::_thesis: verum
end;
hence  X = Y by A10, A17; ::_thesis: verum
end;
consider c, d being Element of AS such that
A18: c in N and
 d in N and
 c <> d by A4, AFF_1:19;
now__::_thesis:_(_M_//_N_implies_X_=_Y_)
assume  M // N ; ::_thesis: X = Y
then  not c in M by A7, A18, AFF_1:45;
then  not LIN a,b,c by A3, A8, A9, A10, Lm7;
hence  X = Y by A1, A2, A5, A6, A8, A9, A18, Th25; ::_thesis: verum
end;
hence  X = Y by A1, A3, A4, A5, A11, Th22; ::_thesis: verum
end;

definition
let AS be AffinSpace;
let a be Element of AS;
let K be Subset of AS;
assume A1: K is being_line ;
funca * K ->  Subset of AS means :Def3: :: AFF_4:def 3
( a in it & K // it );
existence
 ex b1 being Subset of AS st
( a in b1 & K // b1 ) by A1, AFF_1:49;
uniqueness
 for b1, b2 being Subset of AS st a in b1 & K // b1 & a in b2 & K // b2 holds
b1 = b2 by AFF_1:50;
end;

:: 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 b4 being Subset of AS holds
( b4 = a * K iff ( a in b4 & K // b4 ) );

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
proof
let AS be AffinSpace; ::_thesis: for a being Element of AS
for A being Subset of AS st A is being_line holds
a * A is being_line
let a be Element of AS; ::_thesis: for A being Subset of AS st A is being_line holds
a * A is being_line
let A be Subset of AS; ::_thesis: ( A is being_line implies a * A is being_line )
set M = a * A;
assume  A is being_line ; ::_thesis: a * A is being_line
then  A // a * A by Def3;
hence  a * A is being_line by AFF_1:36; ::_thesis: verum
end;

theorem Th28: :: AFF_4:28
for AS being AffinSpace
for a being Element of AS
for X, M 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
let AS be AffinSpace; ::_thesis: for a being Element of AS
for X, M being Subset of AS st X is being_plane & M is being_line & a in X & M c= X holds
a * M c= X
let a be Element of AS; ::_thesis: for X, M being Subset of AS st X is being_plane & M is being_line & a in X & M c= X holds
a * M c= X
let X, M be Subset of AS; ::_thesis: ( X is being_plane & M is being_line & a in X & M c= X implies a * M c= X )
assume that
A1: X is being_plane and
A2: M is being_line and
A3: ( a in X & M c= X ) ; ::_thesis: a * M c= X
set N = a * M;
 ( a in a * M & M // a * M ) by A2, Def3;
hence  a * M c= X by A1, A3, Th23; ::_thesis: verum
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
proof
let AS be AffinSpace; ::_thesis: 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
let a, b, c, d be Element of AS; ::_thesis: 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
let X be Subset of AS; ::_thesis: ( X is being_plane & a in X & b in X & c in X & a,b // c,d & a <> b implies d in X )
assume that
A1: ( X is being_plane & a in X & b in X & c in X ) and
A2: a,b // c,d and
A3: a <> b ; ::_thesis: d in X
set M = Line (a,b);
set N = c * (Line (a,b));
A4: Line (a,b) is being_line by A3, AFF_1:def_3;
then A5: c * (Line (a,b)) c= X by A1, A3, Th19, Th28;
A6: ( a in Line (a,b) & b in Line (a,b) ) by AFF_1:15;
 ( c in c * (Line (a,b)) & Line (a,b) // c * (Line (a,b)) ) by A4, Def3;
then  d in c * (Line (a,b)) by A2, A3, A6, Th7;
hence  d in X by A5; ::_thesis: verum
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 )
proof
let AS be AffinSpace; ::_thesis: 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 )
let a be Element of AS; ::_thesis: for A being Subset of AS st A is being_line holds
( a in A iff a * A = A )
let A be Subset of AS; ::_thesis: ( A is being_line implies ( a in A iff a * A = A ) )
assume A1: A is being_line ; ::_thesis: ( a in A iff a * A = A )
now__::_thesis:_(_a_in_A_implies_a_*_A_=_A_)
assume A2: a in A ; ::_thesis: a * A = A
 A // A by A1, AFF_1:41;
hence  a * A = A by A1, A2, Def3; ::_thesis: verum
end;
hence  ( a in A iff a * A = A ) by A1, Def3; ::_thesis: verum
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)
proof
let AS be AffinSpace; ::_thesis: for a, q being Element of AS
for A being Subset of AS st A is being_line holds
a * A = a * (q * A)
let a, q be Element of AS; ::_thesis: for A being Subset of AS st A is being_line holds
a * A = a * (q * A)
let A be Subset of AS; ::_thesis: ( A is being_line implies a * A = a * (q * A) )
assume A1: A is being_line ; ::_thesis: a * A = a * (q * A)
then  ( A // q * A & A // a * A ) by Def3;
then A2: a * A // q * A by AFF_1:44;
A3: q * A is being_line by A1, Th27;
then A4: a in a * (q * A) by Def3;
 q * A // a * (q * A) by A3, Def3;
then A5: a * A // a * (q * A) by A2, AFF_1:44;
 a in a * A by A1, Def3;
hence  a * A = a * (q * A) by A4, A5, AFF_1:45; ::_thesis: verum
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
let AS be AffinSpace; ::_thesis: for a being Element of AS
for A being Subset of AS st A is being_line & a in A holds
a * A = A
let a be Element of AS; ::_thesis: for A being Subset of AS st A is being_line & a in A holds
a * A = A
let A be Subset of AS; ::_thesis: ( A is being_line & a in A implies a * A = A )
assume that
A1: A is being_line and
A2: a in A ; ::_thesis: a * A = A
 A // A by A1, AFF_1:41;
hence  a * A = A by A1, A2, Def3; ::_thesis: verum
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
proof
let AS be AffinSpace; ::_thesis: for a being Element of AS
for K, M being Subset of AS st K // M holds
a * K = a * M
let a be Element of AS; ::_thesis: for K, M being Subset of AS st K // M holds
a * K = a * M
let K, M be Subset of AS; ::_thesis: ( K // M implies a * K = a * M )
assume A1: K // M ; ::_thesis: a * K = a * M
then A2: K is being_line by AFF_1:36;
then  K // a * K by Def3;
then A3: a * K // M by A1, AFF_1:44;
A4: M is being_line by A1, AFF_1:36;
then A5: a in a * M by Def3;
 M // a * M by A4, Def3;
then A6: a * K // a * M by A3, AFF_1:44;
 a in a * K by A2, Def3;
hence  a * K = a * M by A5, A6, AFF_1:45; ::_thesis: verum
end;

definition
let AS be AffinSpace;
let X, Y be Subset of AS;
predX '||' Y means :Def4: :: 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;
end;

:: deftheorem Def4 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 );

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
proof
let AS be AffinSpace; ::_thesis: 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
let X, Y be Subset of AS; ::_thesis: ( X c= Y & ( ( X is being_line & Y is being_line ) or ( X is being_plane & Y is being_plane ) ) implies X = Y )
assume that
A1: X c= Y and
A2: ( ( X is being_line & Y is being_line ) or ( X is being_plane & Y is being_plane ) ) ; ::_thesis: X = Y
A3: now__::_thesis:_(_X_is_being_plane_&_Y_is_being_plane_implies_X_=_Y_)
assume that
A4: X is being_plane and
A5: Y is being_plane ; ::_thesis: X = Y
consider K, P being Subset of AS such that
A6: K is being_line and
A7: P is being_line and
A8: not K // P and
A9: X = Plane (K,P) by A4, Def2;
consider a, b being Element of AS such that
A10: a in P and
 b in P and
 a <> b by A7, AFF_1:19;
set M = a * K;
A11: K // a * K by A6, Def3;
A12: P c= X by A6, A9, Th14;
then A13: P c= Y by A1, XBOOLE_1:1;
A14: a * K is being_line by A6, Th27;
 ( a in a * K & P c= Plane (K,P) ) by A6, Def3, Th14;
then A15: a * K c= X by A9, A10, A11, Lm4;
then  a * K c= Y by A1, XBOOLE_1:1;
hence  X = Y by A4, A5, A7, A8, A11, A14, A12, A13, A15, Th26; ::_thesis: verum
end;
now__::_thesis:_(_X_is_being_line_&_Y_is_being_line_implies_X_=_Y_)
assume that
A16: X is being_line and
A17: Y is being_line ; ::_thesis: X = Y
consider a, b being Element of AS such that
A18: a <> b and
A19: X = Line (a,b) by A16, AFF_1:def_3;
 ( a in X & b in X ) by A19, AFF_1:15;
hence  X = Y by A1, A17, A18, A19, AFF_1:57; ::_thesis: verum
end;
hence  X = Y by A2, A3; ::_thesis: verum
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 )
proof
let AS be AffinSpace; ::_thesis: 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 )
let X be Subset of AS; ::_thesis: ( X is being_plane implies ex a, b, c being Element of AS st
( a in X & b in X & c in X & not LIN a,b,c ) )
assume  X is being_plane ; ::_thesis: ex a, b, c being Element of AS st
( a in X & b in X & c in X & not LIN a,b,c )
then consider K, P being Subset of AS such that
A1: K is being_line and
A2: P is being_line and
A3: not K // P and
A4: X = Plane (K,P) by Def2;
consider a, b being Element of AS such that
A5: a in P and
A6: b in P and
A7: a <> b by A2, AFF_1:19;
set Q = a * K;
consider c being Element of AS such that
A8: a <> c and
A9: c in a * K by A1, Th27, AFF_1:20;
take  a ; ::_thesis: ex b, c being Element of AS st
( a in X & b in X & c in X & not LIN a,b,c )
take  b ; ::_thesis: ex c being Element of AS st
( a in X & b in X & c in X & not LIN a,b,c )
take  c ; ::_thesis: ( a in X & b in X & c in X & not LIN a,b,c )
A10: P c= Plane (K,P) by A1, Th14;
hence  ( a in X & b in X ) by A4, A5, A6; ::_thesis: ( c in X & not LIN a,b,c )
A11: ( K // a * K & a in a * K ) by A1, Def3;
then  a * K c= Plane (K,P) by A5, A10, Lm4;
hence  c in X by A4, A9; ::_thesis: not LIN a,b,c
A12: a * K is being_line by A1, Th27;
thus  not LIN a,b,c ::_thesis: verum
proof
assume  LIN a,b,c ; ::_thesis: contradiction
then  c in P by A2, A5, A6, A7, AFF_1:25;
hence  contradiction by A2, A3, A5, A11, A12, A8, A9, AFF_1:18; ::_thesis: verum
end;
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
let AS be AffinSpace; ::_thesis: 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 )
let a be Element of AS; ::_thesis: 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 )
let X be Subset of AS; ::_thesis: ( X is being_plane implies ex b, c being Element of AS st
( b in X & c in X & not LIN a,b,c ) )
assume  X is being_plane ; ::_thesis: ex b, c being Element of AS st
( b in X & c in X & not LIN a,b,c )
then consider p, q, r being Element of AS such that
A1: ( p in X & q in X ) and
A2: r in X and
A3: not LIN p,q,r by Th34;
now__::_thesis:_(_LIN_a,r,p_&_LIN_a,r,q_implies_ex_b,_c_being_Element_of_AS_st_
(_b_in_X_&_c_in_X_&_not_LIN_a,b,c_)_)
assume A4: ( LIN a,r,p & LIN a,r,q ) ; ::_thesis: ex b, c being Element of AS st
( b in X & c in X & not LIN a,b,c )
take b = p; ::_thesis: ex c being Element of AS st
( b in X & c in X & not LIN a,b,c )
take c = q; ::_thesis: ( b in X & c in X & not LIN a,b,c )
thus  ( b in X & c in X ) by A1; ::_thesis: not LIN a,b,c
 LIN a,r,r by AFF_1:7;
then  a = r by A3, A4, AFF_1:8;
hence  not LIN a,b,c by A3, AFF_1:6; ::_thesis: verum
end;
hence  ex b, c being Element of AS st
( b in X & c in X & not LIN a,b,c ) by A1, A2; ::_thesis: verum
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 )
proof
let AS be AffinSpace; ::_thesis: 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 )
let M, X be Subset of AS; ::_thesis: ( M is being_line & X is being_plane implies ex q being Element of AS st
( q in X & not q in M ) )
assume that
A1: M is being_line and
A2: X is being_plane ; ::_thesis: ex q being Element of AS st
( q in X & not q in M )
consider a, b, c being Element of AS such that
A3: ( a in X & b in X ) and
A4: c in X and
A5: not LIN a,b,c by A2, Th34;
assume A6: for q being Element of AS holds
( not q in X or q in M ) ; ::_thesis: contradiction
then A7: c in M by A4;
 ( a in M & b in M ) by A6, A3;
hence  contradiction by A1, A5, A7, AFF_1:21; ::_thesis: verum
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 )
proof
let AS be AffinSpace; ::_thesis: 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 )
let a be Element of AS; ::_thesis: 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 )
let A be Subset of AS; ::_thesis: ( A is being_line implies ex X being Subset of AS st
( a in X & A c= X & X is being_plane ) )
assume A1: A is being_line ; ::_thesis: ex X being Subset of AS st
( a in X & A c= X & X is being_plane )
then consider p, q being Element of AS such that
A2: p in A and
 q in A and
 p <> q by AFF_1:19;
A3: now__::_thesis:_(_a_in_A_implies_ex_X_being_Subset_of_AS_st_
(_a_in_X_&_A_c=_X_&_X_is_being_plane_)_)
consider b being Element of AS such that
A4: not b in A by A1, Th12;
consider P being Subset of AS such that
A5: ( a in P & b in P ) and
A6: P is being_line by Th11;
set X = Plane (P,A);
A7: A c= Plane (P,A) by A6, Th14;
assume A8: a in A ; ::_thesis: ex X being Subset of AS st
( a in X & A c= X & X is being_plane )
then  not P // A by A4, A5, AFF_1:45;
then  Plane (P,A) is being_plane by A1, A6, Def2;
hence  ex X being Subset of AS st
( a in X & A c= X & X is being_plane ) by A8, A7; ::_thesis: verum
end;
now__::_thesis:_(_not_a_in_A_implies_ex_X_being_Subset_of_AS_st_
(_a_in_X_&_A_c=_X_&_X_is_being_plane_)_)
consider P being Subset of AS such that
A9: a in P and
A10: p in P and
A11: P is being_line by Th11;
set X = Plane (P,A);
 A c= Plane (P,A) by A11, Th14;
then A12: P c= Plane (P,A) by A2, A10, A11, Lm4, AFF_1:41;
assume  not a in A ; ::_thesis: ex X being Subset of AS st
( a in X & A c= X & X is being_plane )
then  not P // A by A2, A9, A10, AFF_1:45;
then  Plane (P,A) is being_plane by A1, A11, Def2;
hence  ex X being Subset of AS st
( a in X & A c= X & X is being_plane ) by A9, A11, A12, Th14; ::_thesis: verum
end;
hence  ex X being Subset of AS st
( a in X & A c= X & X is being_plane ) by A3; ::_thesis: verum
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 )
proof
let AS be AffinSpace; ::_thesis: 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 )
let a, b, c be Element of AS; ::_thesis: ex X being Subset of AS st
( a in X & b in X & c in X & X is being_plane )
consider A being Subset of AS such that
A1: ( a in A & b in A ) and
A2: A is being_line by Th11;
 ex X being Subset of AS st
( c in X & A c= X & X is being_plane ) by A2, Th36;
hence  ex X being Subset of AS st
( a in X & b in X & c in X & X is being_plane ) by A1; ::_thesis: verum
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 )
proof
let AS be AffinSpace; ::_thesis: 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 )
let q be Element of AS; ::_thesis: 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 )
let M, N be Subset of AS; ::_thesis: ( q in M & q in N & M is being_line & N is being_line implies ex X being Subset of AS st
( M c= X & N c= X & X is being_plane ) )
assume that
A1: q in M and
A2: q in N and
A3: M is being_line and
A4: N is being_line ; ::_thesis: ex X being Subset of AS st
( M c= X & N c= X & X is being_plane )
consider a being Element of AS such that
A5: a <> q and
A6: a in N by A4, AFF_1:20;
A7: ex X being Subset of AS st
( a in X & M c= X & X is being_plane ) by A3, Th36;
 N = Line (q,a) by A2, A4, A5, A6, AFF_1:24;
hence  ex X being Subset of AS st
( M c= X & N c= X & X is being_plane ) by A1, A5, A7, Th19; ::_thesis: verum
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 )
proof
let AS be AffinSpace; ::_thesis: 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 )
let M, N be Subset of AS; ::_thesis: ( M // N implies ex X being Subset of AS st
( M c= X & N c= X & X is being_plane ) )
assume A1: M // N ; ::_thesis: ex X being Subset of AS st
( M c= X & N c= X & X is being_plane )
then  N is being_line by AFF_1:36;
then consider a, b being Element of AS such that
A2: a in N and
 b in N and
 a <> b by AFF_1:19;
A3: M is being_line by A1, AFF_1:36;
then A4: ex X being Subset of AS st
( a in X & M c= X & X is being_plane ) by Th36;
 N = a * M by A1, A3, A2, Def3;
hence  ex X being Subset of AS st
( M c= X & N c= X & X is being_plane ) by A3, A4, Th28; ::_thesis: verum
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 )
proof
let AS be AffinSpace; ::_thesis: for M, N being Subset of AS st M is being_line & N is being_line holds
( M // N iff M '||' N )
let M, N be Subset of AS; ::_thesis: ( M is being_line & N is being_line implies ( M // N iff M '||' N ) )
assume that
A1: M is being_line and
A2: N is being_line ; ::_thesis: ( M // N iff M '||' N )
A3: now__::_thesis:_(_M_//_N_implies_M_'||'_N_)
assume A4: M // N ; ::_thesis: M '||' N
now__::_thesis:_for_a_being_Element_of_AS
for_A_being_Subset_of_AS_st_a_in_N_&_A_is_being_line_&_A_c=_M_holds_
a_*_A_c=_N
let a be Element of AS; ::_thesis: for A being Subset of AS st a in N & A is being_line & A c= M holds
a * A c= N
let A be Subset of AS; ::_thesis: ( a in N & A is being_line & A c= M implies a * A c= N )
assume that
A5: a in N and
A6: ( A is being_line & A c= M ) ; ::_thesis: a * A c= N
 N = a * M by A1, A4, A5, Def3;
hence  a * A c= N by A1, A6, Th33; ::_thesis: verum
end;
hence  M '||' N by Def4; ::_thesis: verum
end;
now__::_thesis:_(_M_'||'_N_implies_M_//_N_)
consider a, b being Element of AS such that
A7: a in N and
 b in N and
 a <> b by A2, AFF_1:19;
A8: a * M is being_line by A1, Th27;
assume  M '||' N ; ::_thesis: M // N
then  a * M c= N by A1, A7, Def4;
then  a * M = N by A2, A8, Th33;
hence  M // N by A1, Def3; ::_thesis: verum
end;
hence  ( M // N iff M '||' N ) by A3; ::_thesis: verum
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 ) ) )
proof
let AS be AffinSpace; ::_thesis: 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 ) ) )
let M, X be Subset of AS; ::_thesis: ( M is being_line & X is being_plane implies ( M '||' X iff ex N being Subset of AS st
( N c= X & ( M // N or N // M ) ) ) )
assume that
A1: M is being_line and
A2: X is being_plane ; ::_thesis: ( M '||' X iff ex N being Subset of AS st
( N c= X & ( M // N or N // M ) ) )
A3: now__::_thesis:_(_ex_N_being_Subset_of_AS_st_
(_N_c=_X_&_(_M_//_N_or_N_//_M_)_)_implies_M_'||'_X_)
given N being Subset of AS such that A4: N c= X and
A5: ( M // N or N // M ) ; ::_thesis: M '||' X
now__::_thesis:_for_a_being_Element_of_AS
for_A_being_Subset_of_AS_st_a_in_X_&_A_is_being_line_&_A_c=_M_holds_
a_*_A_c=_X
let a be Element of AS; ::_thesis: for A being Subset of AS st a in X & A is being_line & A c= M holds
a * A c= X
let A be Subset of AS; ::_thesis: ( a in X & A is being_line & A c= M implies a * A c= X )
assume that
A6: a in X and
A7: A is being_line and
A8: A c= M ; ::_thesis: a * A c= X
 A = M by A1, A7, A8, Th33;
then  M // a * A by A7, Def3;
then A9: N // a * A by A5, AFF_1:44;
 a in a * A by A7, Def3;
hence  a * A c= X by A2, A4, A6, A9, Th23; ::_thesis: verum
end;
hence  M '||' X by Def4; ::_thesis: verum
end;
now__::_thesis:_(_M_'||'_X_implies_ex_N_being_Subset_of_AS_st_
(_N_c=_X_&_(_M_//_N_or_N_//_M_)_)_)
consider a, b, c being Element of AS such that
A10: a in X and
 b in X and
 c in X and
 not LIN a,b,c by A2, Th34;
assume A11: M '||' X ; ::_thesis: ex N being Subset of AS st
( N c= X & ( M // N or N // M ) )
take N = a * M; ::_thesis: ( N c= X & ( M // N or N // M ) )
thus  N c= X by A1, A11, A10, Def4; ::_thesis: ( M // N or N // M )
thus  ( M // N or N // M ) by A1, Def3; ::_thesis: verum
end;
hence  ( M '||' X iff ex N being Subset of AS st
( N c= X & ( M // N or N // M ) ) ) by A3; ::_thesis: verum
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
proof
let AS be AffinSpace; ::_thesis: for M, X being Subset of AS st M is being_line & X is being_plane & M c= X holds
M '||' X
let M, X be Subset of AS; ::_thesis: ( M is being_line & X is being_plane & M c= X implies M '||' X )
assume that
A1: M is being_line and
A2: ( X is being_plane & M c= X ) ; ::_thesis: M '||' X
 M // M by A1, AFF_1:41;
hence  M '||' X by A1, A2, Th41; ::_thesis: verum
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
proof
let AS be AffinSpace; ::_thesis: 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
let a be Element of AS; ::_thesis: 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
let A, X be Subset of AS; ::_thesis: ( A is being_line & X is being_plane & a in A & a in X & A '||' X implies A c= X )
assume that
A1: A is being_line and
A2: X is being_plane and
A3: a in A and
A4: a in X and
A5: A '||' X ; ::_thesis: A c= X
consider N being Subset of AS such that
A6: N c= X and
A7: ( A // N or N // A ) by A1, A2, A5, Th41;
A8: N is being_line by A7, AFF_1:36;
A = a * A by A1, A3, Lm8
.= a * N by A7, Th32 ;
hence  A c= X by A2, A4, A6, A8, Th28; ::_thesis: verum
end;

definition
let AS be AffinSpace;
let K, M, N be Subset of AS;
predK,M,N is_coplanar  means :Def5: :: AFF_4:def 5
 ex X being Subset of AS st
( K c= X & M c= X & N c= X & X is being_plane );
end;

:: deftheorem Def5 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 ) );

theorem Th44: :: 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 )
proof
let AS be AffinSpace; ::_thesis: 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 )
let K, M, N be Subset of AS; ::_thesis: ( K,M,N is_coplanar implies ( 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 ) )
assume  K,M,N is_coplanar ; ::_thesis: ( 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 )
then  ex X being Subset of AS st
( K c= X & M c= X & N c= X & X is being_plane ) by Def5;
hence  ( 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 ) by Def5; ::_thesis: verum
end;

theorem :: AFF_4:45
for AS being AffinSpace
for M, N, K, A 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
let AS be AffinSpace; ::_thesis: for M, N, K, A 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
let M, N, K, A be Subset of AS; ::_thesis: ( M is being_line & N is being_line & M,N,K is_coplanar & M,N,A is_coplanar & M <> N implies M,K,A is_coplanar )
assume that
A1: ( M is being_line & N is being_line ) and
A2: M,N,K is_coplanar and
A3: M,N,A is_coplanar and
A4: M <> N ; ::_thesis: M,K,A is_coplanar
consider X being Subset of AS such that
A5: M c= X and
A6: N c= X and
A7: K c= X and
A8: X is being_plane by A2, Def5;
 ex Y being Subset of AS st
( M c= Y & N c= Y & A c= Y & Y is being_plane ) by A3, Def5;
then  A c= X by A1, A4, A5, A6, A8, Th26;
hence  M,K,A is_coplanar by A5, A7, A8, Def5; ::_thesis: verum
end;

theorem Th46: :: AFF_4:46
for AS being AffinSpace
for K, M, X, A 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 )
proof
let AS be AffinSpace; ::_thesis: for K, M, X, A 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 )
let K, M, X, A be Subset of AS; ::_thesis: ( K is being_line & M is being_line & X is being_plane & K c= X & M c= X & K <> M implies ( K,M,A is_coplanar iff A c= X ) )
assume that
A1: ( K is being_line & M is being_line ) and
A2: ( X is being_plane & K c= X & M c= X ) and
A3: K <> M ; ::_thesis: ( K,M,A is_coplanar iff A c= X )
now__::_thesis:_(_K,M,A_is_coplanar_implies_A_c=_X_)
assume  K,M,A is_coplanar ; ::_thesis: A c= X
then  ex Y being Subset of AS st
( K c= Y & M c= Y & A c= Y & Y is being_plane ) by Def5;
hence  A c= X by A1, A2, A3, Th26; ::_thesis: verum
end;
hence  ( K,M,A is_coplanar iff A c= X ) by A2, Def5; ::_thesis: verum
end;

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 )
proof
let AS be AffinSpace; ::_thesis: 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 )
let q be Element of AS; ::_thesis: 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 )
let K, M be Subset of AS; ::_thesis: ( q in K & q in M & K is being_line & M is being_line implies ( K,M,M is_coplanar & M,K,M is_coplanar & M,M,K is_coplanar ) )
assume  ( q in K & q in M & K is being_line & M is being_line ) ; ::_thesis: ( K,M,M is_coplanar & M,K,M is_coplanar & M,M,K is_coplanar )
then  ex X being Subset of AS st
( K c= X & M c= X & X is being_plane ) by Th38;
hence  ( K,M,M is_coplanar & M,K,M is_coplanar & M,M,K is_coplanar ) by Def5; ::_thesis: verum
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
proof
let AS be AffinSpace; ::_thesis: 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
let X be Subset of AS; ::_thesis: ( AS is not AffinPlane & X is being_plane implies ex q being Element of AS st not q in X )
assume that
A1: AS is not AffinPlane and
A2: X is being_plane ; ::_thesis: not for q being Element of AS holds q in X
assume A3: for q being Element of AS holds q in X ; ::_thesis: contradiction
 for a, b, c, d being Element of AS st not a,b // c,d holds
ex q being Element of AS st
( a,b // a,q & c,d // c,q )
proof
let a, b, c, d be Element of AS; ::_thesis: ( not a,b // c,d implies ex q being Element of AS st
( a,b // a,q & c,d // c,q ) )
set M = Line (a,b);
set N = Line (c,d);
A4: ( a in Line (a,b) & b in Line (a,b) ) by AFF_1:15;
A5: ( c in Line (c,d) & d in Line (c,d) ) by AFF_1:15;
assume A6: not a,b // c,d ; ::_thesis: ex q being Element of AS st
( a,b // a,q & c,d // c,q )
then A7: a <> b by AFF_1:3;
then A8: Line (a,b) is being_line by AFF_1:def_3;
A9: c <> d by A6, AFF_1:3;
then A10: Line (c,d) is being_line by AFF_1:def_3;
 ( c in X & d in X ) by A3;
then A11: Line (c,d) c= X by A2, A9, Th19;
 ( a in X & b in X ) by A3;
then  Line (a,b) c= X by A2, A7, Th19;
then consider q being Element of AS such that
A12: q in Line (a,b) and
A13: q in Line (c,d) by A2, A6, A11, A8, A10, A4, A5, Th22, AFF_1:39;
 LIN c,d,q by A10, A5, A13, AFF_1:21;
then A14: c,d // c,q by AFF_1:def_1;
 LIN a,b,q by A8, A4, A12, AFF_1:21;
then  a,b // a,q by AFF_1:def_1;
hence  ex q being Element of AS st
( a,b // a,q & c,d // c,q ) by A14; ::_thesis: verum
end;
hence  contradiction by A1, DIRAF:def_7; ::_thesis: verum
end;

Lm10:  for AS being AffinSpace
for q, a, b, c, a9, b9, c9 being Element of AS
for A, P, C 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
let AS be AffinSpace; ::_thesis: for q, a, b, c, a9, b9, c9 being Element of AS
for A, P, C 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
let q, a, b, c, a9, b9, c9 be Element of AS; ::_thesis: for A, P, C 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
let A, P, C be Subset of AS; ::_thesis: ( 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 implies b,c // b9,c9 )
assume that
A1: q in A and
A2: q in P and
A3: q in C and
A4: not A,P,C is_coplanar and
A5: q <> a and
A6: q <> b and
A7: q <> c and
A8: a in A and
A9: a9 in A and
A10: b in P and
A11: b9 in P and
A12: c in C and
A13: c9 in C and
A14: A is being_line and
A15: P is being_line and
A16: C is being_line and
A17: A <> P and
A18: A <> C and
A19: a,b // a9,b9 and
A20: a,c // a9,c9 ; ::_thesis: b,c // b9,c9
A21: c <> a by A1, A3, A5, A8, A12, A14, A16, A18, AFF_1:18;
A22: P <> C by A1, A2, A4, A14, A15, Th47;
then A23: b <> c by A2, A3, A6, A10, A12, A15, A16, AFF_1:18;
consider X being Subset of AS such that
A24: ( P c= X & C c= X ) and
A25: X is being_plane by A2, A3, A15, A16, Th38;
consider Y being Subset of AS such that
A26: A c= Y and
A27: C c= Y and
A28: Y is being_plane by A1, A3, A14, A16, Th38;
A29: a <> b by A1, A2, A5, A8, A10, A14, A15, A17, AFF_1:18;
A30: now__::_thesis:_(_q_<>_a9_implies_b,c_//_b9,c9_)
assume A31: q <> a9 ; ::_thesis: b,c // b9,c9
then A32: q <> c9 by A1, A3, A5, A7, A8, A9, A12, A14, A16, A18, A20, Th8;
A33: now__::_thesis:_(_a_<>_a9_implies_b,c_//_b9,c9_)
set BC = Line (b,c);
set BC9 = Line (b9,c9);
set AB = Line (a,b);
set AB9 = Line (a9,b9);
set AC = Line (a,c);
set AC9 = Line (a9,c9);
assume A34: a <> a9 ; ::_thesis: b,c // b9,c9
assume A35: not b,c // b9,c9 ; ::_thesis: contradiction
A36: ( b9 in Line (b9,c9) & c9 in Line (b9,c9) ) by AFF_1:15;
A37: Line (b,c) c= X by A10, A12, A24, A25, A23, Th19;
A38: c in Line (b,c) by AFF_1:15;
A39: ( Line (b,c) is being_line & b in Line (b,c) ) by A23, AFF_1:15, AFF_1:def_3;
A40: c9 <> b9 by A2, A3, A11, A13, A15, A16, A22, A32, AFF_1:18;
then A41: Line (b9,c9) is being_line by AFF_1:def_3;
 Line (b9,c9) c= X by A11, A13, A24, A25, A40, Th19;
then consider p being Element of AS such that
A42: p in Line (b,c) and
A43: p in Line (b9,c9) by A25, A35, A41, A39, A38, A36, A37, Th22, AFF_1:39;
A44: a9 in Line (a9,c9) by AFF_1:15;
 LIN c9,b9,p by A41, A36, A43, AFF_1:21;
then consider y being Element of AS such that
A45: LIN c9,a9,y and
A46: b9,a9 // p,y by A40, Th1;
A47: c in Line (a,c) by AFF_1:15;
 LIN c,b,p by A39, A38, A42, AFF_1:21;
then consider x being Element of AS such that
A48: LIN c,a,x and
A49: b,a // p,x by A23, Th1;
A50: a in Line (a,b) by AFF_1:15;
A51: ( Line (a,c) is being_line & a in Line (a,c) ) by A21, AFF_1:15, AFF_1:def_3;
then A52: x in Line (a,c) by A21, A47, A48, AFF_1:25;
set K = p * (Line (a,b));
A53: b in Line (a,b) by AFF_1:15;
A54: Line (a,b) is being_line by A29, AFF_1:def_3;
then A55: Line (a,b) // p * (Line (a,b)) by Def3;
A56: p in p * (Line (a,b)) by A54, Def3;
 p,x // a,b by A49, AFF_1:4;
then  p,x // Line (a,b) by A29, AFF_1:def_4;
then  p,x // p * (Line (a,b)) by A55, Th3;
then A57: x in p * (Line (a,b)) by A56, Th2;
A58: a9 <> b9 by A1, A2, A9, A11, A14, A15, A17, A31, AFF_1:18;
 p,y // a9,b9 by A46, AFF_1:4;
then A59: p,y // Line (a9,b9) by A58, AFF_1:def_4;
 Line (a,b) // Line (a9,b9) by A19, A29, A58, AFF_1:37;
then  Line (a9,b9) // p * (Line (a,b)) by A55, AFF_1:44;
then  p,y // p * (Line (a,b)) by A59, Th3;
then A60: y in p * (Line (a,b)) by A56, Th2;
A61: Line (a,c) c= Y by A8, A12, A26, A27, A28, A21, Th19;
A62: c9 in Line (a9,c9) by AFF_1:15;
A63: a9 <> c9 by A1, A3, A9, A13, A14, A16, A18, A31, AFF_1:18;
then  Line (a9,c9) is being_line by AFF_1:def_3;
then A64: y in Line (a9,c9) by A63, A44, A62, A45, AFF_1:25;
A65: Line (a9,c9) c= Y by A9, A13, A26, A27, A28, A63, Th19;
A66: now__::_thesis:_not_x_<>_y
assume A67: x <> y ; ::_thesis: contradiction
then  p * (Line (a,b)) = Line (x,y) by A54, A57, A60, Th27, AFF_1:57;
then  p * (Line (a,b)) c= Y by A28, A61, A65, A52, A64, A67, Th19;
then A68: Line (a,b) c= Y by A8, A26, A28, A50, A55, Th23;
 P = Line (q,b) by A2, A6, A10, A15, AFF_1:57;
then  P c= Y by A1, A6, A26, A28, A53, A68, Th19;
hence  contradiction by A4, A26, A27, A28, Def5; ::_thesis: verum
end;
A69: Line (a,c) // Line (a9,c9) by A20, A21, A63, AFF_1:37;
now__::_thesis:_not_x_=_y
assume  x = y ; ::_thesis: contradiction
then  a9 in Line (a,c) by A44, A69, A52, A64, AFF_1:45;
then  c in A by A8, A9, A14, A34, A51, A47, AFF_1:18;
hence  contradiction by A1, A3, A7, A12, A14, A16, A18, AFF_1:18; ::_thesis: verum
end;
hence  contradiction by A66; ::_thesis: verum
end;
now__::_thesis:_(_a_=_a9_implies_b,c_//_b9,c9_)
assume  a = a9 ; ::_thesis: b,c // b9,c9
then  ( b = b9 & c = c9 ) by A1, A2, A3, A5, A6, A7, A8, A10, A11, A12, A13, A14, A15, A16, A17, A18, A19, A20, Th9;
hence  b,c // b9,c9 by AFF_1:2; ::_thesis: verum
end;
hence  b,c // b9,c9 by A33; ::_thesis: verum
end;
now__::_thesis:_(_q_=_a9_implies_b,c_//_b9,c9_)
assume  q = a9 ; ::_thesis: b,c // b9,c9
then  ( q = b9 & q = c9 ) by A1, A2, A3, A5, A6, A7, A8, A10, A11, A12, A13, A14, A15, A16, A17, A18, A19, A20, Th8;
hence  b,c // b9,c9 by AFF_1:3; ::_thesis: verum
end;
hence  b,c // b9,c9 by A30; ::_thesis: verum
end;

theorem Th49: :: AFF_4:49
for AS being AffinSpace
for q, a, b, c, a9, b9, c9 being Element of AS
for A, P, C 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
let AS be AffinSpace; ::_thesis: for q, a, b, c, a9, b9, c9 being Element of AS
for A, P, C 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
let q, a, b, c, a9, b9, c9 be Element of AS; ::_thesis: for A, P, C 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
let A, P, C be Subset of AS; ::_thesis: ( 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 implies b,c // b9,c9 )
assume that
A1: AS is not AffinPlane and
A2: q in A and
A3: q in P and
A4: q in C and
A5: q <> a and
A6: q <> b and
A7: q <> c and
A8: ( a in A & a9 in A ) and
A9: ( b in P & b9 in P ) and
A10: ( c in C & c9 in C ) and
A11: A is being_line and
A12: P is being_line and
A13: C is being_line and
A14: A <> P and
A15: A <> C and
A16: a,b // a9,b9 and
A17: a,c // a9,c9 ; ::_thesis: b,c // b9,c9
now__::_thesis:_(_A,P,C_is_coplanar_implies_b,c_//_b9,c9_)
assume  A,P,C is_coplanar ; ::_thesis: b,c // b9,c9
then consider X being Subset of AS such that
A18: A c= X and
A19: P c= X and
A20: C c= X and
A21: X is being_plane by Def5;
consider d being Element of AS such that
A22: not d in X by A1, A21, Th48;
 LIN q,a,a9 by A2, A8, A11, AFF_1:21;
then consider d9 being Element of AS such that
A23: LIN q,d,d9 and
A24: a,d // a9,d9 by A5, Th1;
set K = Line (q,d);
A25: d in Line (q,d) by AFF_1:15;
then A26: not Line (q,d) c= X by A22;
A27: q <> d by A2, A18, A22;
then A28: ( q in Line (q,d) & Line (q,d) is being_line ) by AFF_1:15, AFF_1:def_3;
then A29: d9 in Line (q,d) by A25, A27, A23, AFF_1:25;
now__::_thesis:_(_P_<>_C_implies_b,c_//_b9,c9_)
assume A30: P <> C ; ::_thesis: b,c // b9,c9
A31: not Line (q,d),P,C is_coplanar
proof
assume  Line (q,d),P,C is_coplanar ; ::_thesis: contradiction
then  P,C, Line (q,d) is_coplanar by Th44;
hence  contradiction by A12, A13, A19, A20, A21, A26, A30, Th46; ::_thesis: verum
end;
A32: Line (q,d) <> A by A18, A22, A25;
 not A, Line (q,d),P is_coplanar
proof
assume  A, Line (q,d),P is_coplanar ; ::_thesis: contradiction
then  A,P, Line (q,d) is_coplanar by Th44;
hence  contradiction by A11, A12, A14, A18, A19, A21, A26, Th46; ::_thesis: verum
end;
then A33: d,b // d9,b9 by A2, A3, A5, A6, A8, A9, A11, A12, A14, A16, A25, A27, A28, A24, A29, A32, Lm10;
A34: ( Line (q,d) <> P & Line (q,d) <> C ) by A19, A20, A22, A25;
 not A, Line (q,d),C is_coplanar
proof
assume  A, Line (q,d),C is_coplanar ; ::_thesis: contradiction
then  A,C, Line (q,d) is_coplanar by Th44;
hence  contradiction by A11, A13, A15, A18, A20, A21, A26, Th46; ::_thesis: verum
end;
then  d,c // d9,c9 by A2, A4, A5, A7, A8, A10, A11, A13, A15, A17, A25, A27, A28, A24, A29, A32, Lm10;
hence  b,c // b9,c9 by A3, A4, A6, A7, A9, A10, A12, A13, A25, A27, A28, A29, A34, A31, A33, Lm10; ::_thesis: verum
end;
hence  b,c // b9,c9 by A9, A10, A12, AFF_1:51; ::_thesis: verum
end;
hence  b,c // b9,c9 by A2, A3, A4, A5, A6, A7, A8, A9, A10, A11, A12, A13, A14, A15, A16, A17, Lm10; ::_thesis: verum
end;

theorem :: AFF_4:50
for AS being AffinSpace st AS is not AffinPlane holds
AS is Desarguesian
proof
let AS be AffinSpace; ::_thesis: ( AS is not AffinPlane implies AS is Desarguesian )
assume  AS is not AffinPlane ; ::_thesis: AS is Desarguesian
then  for A, P, C being Subset of AS
for q, a, b, c, a9, b9, c9 being Element of AS st 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 by Th49;
hence  AS is Desarguesian by AFF_2:def_4; ::_thesis: verum
end;

Lm11:  for AS being AffinSpace
for a, a9, b, b9, c, c9 being Element of AS
for A, P, C 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
let AS be AffinSpace; ::_thesis: for a, a9, b, b9, c, c9 being Element of AS
for A, P, C 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
let a, a9, b, b9, c, c9 be Element of AS; ::_thesis: for A, P, C 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
let A, P, C be Subset of AS; ::_thesis: ( 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 implies b,c // b9,c9 )
assume that
A1: A // P and
A2: A // C and
A3: not A,P,C is_coplanar and
A4: a in A and
A5: a9 in A and
A6: b in P and
A7: b9 in P and
A8: c in C and
A9: c9 in C and
A10: A is being_line and
A11: A <> P and
A12: A <> C and
A13: a,b // a9,b9 and
A14: a,c // a9,c9 ; ::_thesis: b,c // b9,c9
A15: c <> a by A2, A4, A8, A12, AFF_1:45;
A16: P // C by A1, A2, AFF_1:44;
then consider X being Subset of AS such that
A17: ( P c= X & C c= X ) and
A18: X is being_plane by Th39;
consider Y being Subset of AS such that
A19: A c= Y and
A20: C c= Y and
A21: Y is being_plane by A2, Th39;
A22: P <> C by A3, A19, A20, A21, Def5;
then A23: b <> c by A6, A8, A16, AFF_1:45;
A24: a <> b by A1, A4, A6, A11, AFF_1:45;
A25: now__::_thesis:_(_a_<>_a9_implies_b,c_//_b9,c9_)
set BC = Line (b,c);
set BC9 = Line (b9,c9);
set AB = Line (a,b);
set AB9 = Line (a9,b9);
set AC = Line (a,c);
set AC9 = Line (a9,c9);
assume A26: a <> a9 ; ::_thesis: b,c // b9,c9
assume A27: not b,c // b9,c9 ; ::_thesis: contradiction
A28: ( b9 in Line (b9,c9) & c9 in Line (b9,c9) ) by AFF_1:15;
A29: Line (b,c) c= X by A6, A8, A17, A18, A23, Th19;
A30: c in Line (b,c) by AFF_1:15;
A31: ( Line (b,c) is being_line & b in Line (b,c) ) by A23, AFF_1:15, AFF_1:def_3;
A32: c9 <> b9 by A7, A9, A16, A22, AFF_1:45;
then A33: Line (b9,c9) is being_line by AFF_1:def_3;
 Line (b9,c9) c= X by A7, A9, A17, A18, A32, Th19;
then consider p being Element of AS such that
A34: p in Line (b,c) and
A35: p in Line (b9,c9) by A18, A27, A33, A31, A30, A28, A29, Th22, AFF_1:39;
A36: a9 in Line (a9,c9) by AFF_1:15;
 LIN c9,b9,p by A33, A28, A35, AFF_1:21;
then consider y being Element of AS such that
A37: LIN c9,a9,y and
A38: b9,a9 // p,y by A32, Th1;
A39: c in Line (a,c) by AFF_1:15;
 LIN c,b,p by A31, A30, A34, AFF_1:21;
then consider x being Element of AS such that
A40: LIN c,a,x and
A41: b,a // p,x by A23, Th1;
A42: a in Line (a,b) by AFF_1:15;
A43: ( Line (a,c) is being_line & a in Line (a,c) ) by A15, AFF_1:15, AFF_1:def_3;
then A44: x in Line (a,c) by A15, A39, A40, AFF_1:25;
set K = p * (Line (a,b));
A45: b in Line (a,b) by AFF_1:15;
A46: Line (a,b) is being_line by A24, AFF_1:def_3;
then A47: Line (a,b) // p * (Line (a,b)) by Def3;
A48: p in p * (Line (a,b)) by A46, Def3;
 p,x // a,b by A41, AFF_1:4;
then  p,x // Line (a,b) by A24, AFF_1:def_4;
then  p,x // p * (Line (a,b)) by A47, Th3;
then A49: x in p * (Line (a,b)) by A48, Th2;
A50: a9 <> b9 by A1, A5, A7, A11, AFF_1:45;
 p,y // a9,b9 by A38, AFF_1:4;
then A51: p,y // Line (a9,b9) by A50, AFF_1:def_4;
 Line (a,b) // Line (a9,b9) by A13, A24, A50, AFF_1:37;
then  Line (a9,b9) // p * (Line (a,b)) by A47, AFF_1:44;
then  p,y // p * (Line (a,b)) by A51, Th3;
then A52: y in p * (Line (a,b)) by A48, Th2;
A53: Line (a,c) c= Y by A4, A8, A19, A20, A21, A15, Th19;
A54: c9 in Line (a9,c9) by AFF_1:15;
A55: a9 <> c9 by A2, A5, A9, A12, AFF_1:45;
then  Line (a9,c9) is being_line by AFF_1:def_3;
then A56: y in Line (a9,c9) by A55, A36, A54, A37, AFF_1:25;
A57: Line (a9,c9) c= Y by A5, A9, A19, A20, A21, A55, Th19;
A58: now__::_thesis:_not_x_<>_y
assume A59: x <> y ; ::_thesis: contradiction
then  p * (Line (a,b)) = Line (x,y) by A46, A49, A52, Th27, AFF_1:57;
then  p * (Line (a,b)) c= Y by A21, A53, A57, A44, A56, A59, Th19;
then A60: Line (a,b) c= Y by A4, A19, A21, A42, A47, Th23;
 P = b * A by A1, A6, A10, Def3;
then  P c= Y by A10, A19, A21, A45, A60, Th28;
hence  contradiction by A3, A19, A20, A21, Def5; ::_thesis: verum
end;
A61: Line (a,c) // Line (a9,c9) by A14, A15, A55, AFF_1:37;
now__::_thesis:_not_x_=_y
assume  x = y ; ::_thesis: contradiction
then  a9 in Line (a,c) by A36, A61, A44, A56, AFF_1:45;
then  c in A by A4, A5, A10, A26, A43, A39, AFF_1:18;
hence  contradiction by A2, A8, A12, AFF_1:45; ::_thesis: verum
end;
hence  contradiction by A58; ::_thesis: verum
end;
now__::_thesis:_(_a_=_a9_implies_b,c_//_b9,c9_)
assume  a = a9 ; ::_thesis: b,c // b9,c9
then  ( b = b9 & c = c9 ) by A1, A2, A4, A6, A7, A8, A9, A11, A12, A13, A14, Th10;
hence  b,c // b9,c9 by AFF_1:2; ::_thesis: verum
end;
hence  b,c // b9,c9 by A25; ::_thesis: verum
end;

theorem Th51: :: AFF_4:51
for AS being AffinSpace
for a, a9, b, b9, c, c9 being Element of AS
for A, P, C 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
let AS be AffinSpace; ::_thesis: for a, a9, b, b9, c, c9 being Element of AS
for A, P, C 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
let a, a9, b, b9, c, c9 be Element of AS; ::_thesis: for A, P, C 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
let A, P, C be Subset of AS; ::_thesis: ( 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 implies b,c // b9,c9 )
assume that
A1: AS is not AffinPlane and
A2: A // P and
A3: A // C and
A4: ( a in A & a9 in A ) and
A5: ( b in P & b9 in P ) and
A6: ( c in C & c9 in C ) and
A7: A is being_line and
A8: P is being_line and
A9: C is being_line and
A10: A <> P and
A11: A <> C and
A12: a,b // a9,b9 and
A13: a,c // a9,c9 ; ::_thesis: b,c // b9,c9
now__::_thesis:_(_A,P,C_is_coplanar_implies_b,c_//_b9,c9_)
assume  A,P,C is_coplanar ; ::_thesis: b,c // b9,c9
then consider X being Subset of AS such that
A14: A c= X and
A15: P c= X and
A16: C c= X and
A17: X is being_plane by Def5;
consider d being Element of AS such that
A18: not d in X by A1, A17, Th48;
set K = d * A;
A19: d in d * A by A7, Def3;
then A20: not d * A c= X by A18;
A21: A // d * A by A7, Def3;
 ex d9 being Element of AS st
( d9 in d * A & a,d // a9,d9 )
proof
A22: now__::_thesis:_(_a_<>_a9_implies_ex_d9_being_Element_of_AS_st_
(_d9_in_d_*_A_&_a,d_//_a9,d9_)_)
assume A23: a <> a9 ; ::_thesis: ex d9 being Element of AS st
( d9 in d * A & a,d // a9,d9 )
consider d9 being Element of AS such that
A24: a,a9 // d,d9 and
A25: a,d // a9,d9 by DIRAF:40;
 d,d9 // a,a9 by A24, AFF_1:4;
then  d,d9 // A by A4, A7, A23, AFF_1:27;
then  d,d9 // d * A by A21, Th3;
then  d9 in d * A by A19, Th2;
hence  ex d9 being Element of AS st
( d9 in d * A & a,d // a9,d9 ) by A25; ::_thesis: verum
end;
now__::_thesis:_(_a_=_a9_implies_ex_d9_being_Element_of_AS_st_
(_d9_in_d_*_A_&_a,d_//_a9,d9_)_)
assume A26: a = a9 ; ::_thesis: ex d9 being Element of AS st
( d9 in d * A & a,d // a9,d9 )
take d9 = d; ::_thesis: ( d9 in d * A & a,d // a9,d9 )
thus  d9 in d * A by A7, Def3; ::_thesis: a,d // a9,d9
thus  a,d // a9,d9 by A26, AFF_1:2; ::_thesis: verum
end;
hence  ex d9 being Element of AS st
( d9 in d * A & a,d // a9,d9 ) by A22; ::_thesis: verum
end;
then consider d9 being Element of AS such that
A27: d9 in d * A and
A28: a,d // a9,d9 ;
A29: ( d * A // P & d * A // C ) by A2, A3, A21, AFF_1:44;
now__::_thesis:_(_P_<>_C_implies_b,c_//_b9,c9_)
assume A30: P <> C ; ::_thesis: b,c // b9,c9
A31: not d * A,P,C is_coplanar
proof
assume  d * A,P,C is_coplanar ; ::_thesis: contradiction
then  P,C,d * A is_coplanar by Th44;
hence  contradiction by A8, A9, A15, A16, A17, A20, A30, Th46; ::_thesis: verum
end;
A32: d * A <> A by A14, A18, A19;
 not A,d * A,P is_coplanar
proof
assume  A,d * A,P is_coplanar ; ::_thesis: contradiction
then  A,P,d * A is_coplanar by Th44;
hence  contradiction by A7, A8, A10, A14, A15, A17, A20, Th46; ::_thesis: verum
end;
then A33: d,b // d9,b9 by A2, A4, A5, A7, A10, A12, A19, A21, A27, A28, A32, Lm11;
A34: ( d * A <> P & d * A <> C ) by A15, A16, A18, A19;
 not A,d * A,C is_coplanar
proof
assume  A,d * A,C is_coplanar ; ::_thesis: contradiction
then  A,C,d * A is_coplanar by Th44;
hence  contradiction by A7, A9, A11, A14, A16, A17, A20, Th46; ::_thesis: verum
end;
then  d,c // d9,c9 by A3, A4, A6, A7, A11, A13, A19, A21, A27, A28, A32, Lm11;
hence  b,c // b9,c9 by A5, A6, A7, A19, A29, A27, A34, A31, A33, Lm11, Th27; ::_thesis: verum
end;
hence  b,c // b9,c9 by A5, A6, A8, AFF_1:51; ::_thesis: verum
end;
hence  b,c // b9,c9 by A2, A3, A4, A5, A6, A7, A10, A11, A12, A13, Lm11; ::_thesis: verum
end;

theorem :: AFF_4:52
for AS being AffinSpace st AS is not AffinPlane holds
AS is translational
proof
let AS be AffinSpace; ::_thesis: ( AS is not AffinPlane implies AS is translational )
assume  AS is not AffinPlane ; ::_thesis: AS is translational
then  for A, P, C being Subset of AS
for a, b, c, a9, b9, c9 being Element of AS st 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 by Th51;
hence  AS is translational by AFF_2:def_11; ::_thesis: verum
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 )
proof
let AS be AffinSpace; ::_thesis: 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 )
let a, b, c, a9, b9 be Element of AS; ::_thesis: ( AS is AffinPlane & not LIN a,b,c implies ex c9 being Element of AS st
( a,c // a9,c9 & b,c // b9,c9 ) )
assume that
A1: AS is AffinPlane and
A2: not LIN a,b,c ; ::_thesis: ex c9 being Element of AS st
( a,c // a9,c9 & b,c // b9,c9 )
consider C being Subset of AS such that
A3: ( b in C & c in C ) and
A4: C is being_line by Th11;
consider N being Subset of AS such that
A5: b9 in N and
A6: C // N by A4, AFF_1:49;
A7: N is being_line by A6, AFF_1:36;
consider P being Subset of AS such that
A8: a in P and
A9: c in P and
A10: P is being_line by Th11;
consider M being Subset of AS such that
A11: a9 in M and
A12: P // M by A10, AFF_1:49;
A13: not M // N
proof
assume  M // N ; ::_thesis: contradiction
then  N // P by A12, AFF_1:44;
then  C // P by A6, AFF_1:44;
then  b in P by A3, A9, AFF_1:45;
hence  contradiction by A2, A8, A9, A10, AFF_1:21; ::_thesis: verum
end;
 M is being_line by A12, AFF_1:36;
then consider c9 being Element of AS such that
A14: c9 in M and
A15: c9 in N by A1, A7, A13, AFF_1:58;
A16: b,c // b9,c9 by A3, A5, A6, A15, AFF_1:39;
 a,c // a9,c9 by A8, A9, A11, A12, A14, AFF_1:39;
hence  ex c9 being Element of AS st
( a,c // a9,c9 & b,c // b9,c9 ) by A16; ::_thesis: verum
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
let AS be AffinSpace; ::_thesis: 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 )
let a, b, c, a9, b9 be Element of AS; ::_thesis: 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 )
let X be Subset of AS; ::_thesis: ( 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 implies ex c9 being Element of AS st
( a,c // a9,c9 & b,c // b9,c9 ) )
assume that
A1: not LIN a,b,c and
A2: a,b // a9,b9 and
A3: a in X and
A4: b in X and
A5: c in X and
A6: X is being_plane and
A7: a9 in X ; ::_thesis: ex c9 being Element of AS st
( a,c // a9,c9 & b,c // b9,c9 )
set C = Line (b,c);
set P = Line (a,c);
set P9 = a9 * (Line (a,c));
set C9 = b9 * (Line (b,c));
A8: b <> c by A1, AFF_1:7;
then A9: Line (b,c) is being_line by AFF_1:def_3;
then A10: Line (b,c) // b9 * (Line (b,c)) by Def3;
 a <> b by A1, AFF_1:7;
then  b9 in X by A2, A3, A4, A6, A7, Th29;
then A11: b9 * (Line (b,c)) c= X by A4, A5, A6, A8, A9, Th19, Th28;
A12: c in Line (a,c) by AFF_1:15;
A13: b9 * (Line (b,c)) is being_line by A9, Th27;
A14: a in Line (a,c) by AFF_1:15;
A15: c <> a by A1, AFF_1:7;
then A16: Line (a,c) is being_line by AFF_1:def_3;
then A17: a9 * (Line (a,c)) is being_line by Th27;
A18: ( b in Line (b,c) & c in Line (b,c) ) by AFF_1:15;
A19: Line (a,c) // a9 * (Line (a,c)) by A16, Def3;
A20: not b9 * (Line (b,c)) // a9 * (Line (a,c))
proof
assume  b9 * (Line (b,c)) // a9 * (Line (a,c)) ; ::_thesis: contradiction
then  b9 * (Line (b,c)) // Line (a,c) by A19, AFF_1:44;
then  Line (b,c) // Line (a,c) by A10, AFF_1:44;
then  b in Line (a,c) by A12, A18, AFF_1:45;
hence  contradiction by A1, A14, A12, A16, AFF_1:21; ::_thesis: verum
end;
 a9 * (Line (a,c)) c= X by A3, A5, A6, A7, A15, A16, Th19, Th28;
then consider c9 being Element of AS such that
A21: c9 in b9 * (Line (b,c)) and
A22: c9 in a9 * (Line (a,c)) by A6, A17, A13, A20, A11, Th22;
 b9 in b9 * (Line (b,c)) by A9, Def3;
then A23: b,c // b9,c9 by A18, A10, A21, AFF_1:39;
 a9 in a9 * (Line (a,c)) by A16, Def3;
then  a,c // a9,c9 by A14, A12, A19, A22, AFF_1:39;
hence  ex c9 being Element of AS st
( a,c // a9,c9 & b,c // b9,c9 ) by A23; ::_thesis: verum
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 )
proof
let AS be AffinSpace; ::_thesis: 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 )
let a, b, c, a9, b9 be Element of AS; ::_thesis: ( not LIN a,b,c & a9 <> b9 & a,b // a9,b9 implies ex c9 being Element of AS st
( a,c // a9,c9 & b,c // b9,c9 ) )
assume that
A1: not LIN a,b,c and
A2: a9 <> b9 and
A3: a,b // a9,b9 ; ::_thesis: ex c9 being Element of AS st
( a,c // a9,c9 & b,c // b9,c9 )
now__::_thesis:_(_AS_is_not_AffinPlane_implies_ex_c9_being_Element_of_AS_st_
(_a,c_//_a9,c9_&_b,c_//_b9,c9_)_)
consider X being Subset of AS such that
A4: a in X and
A5: b in X and
A6: c in X and
A7: X is being_plane by Th37;
assume A8: AS is not AffinPlane ; ::_thesis: ex c9 being Element of AS st
( a,c // a9,c9 & b,c // b9,c9 )
now__::_thesis:_(_not_a9_in_X_implies_ex_c9_being_Element_of_AS_st_
(_a,c_//_a9,c9_&_b,c_//_b9,c9_)_)
set A = Line (a,a9);
set P = Line (b,b9);
set AB = Line (a,b);
set AB9 = Line (a9,b9);
A9: a in Line (a,b) by AFF_1:15;
assume A10: not a9 in X ; ::_thesis: ex c9 being Element of AS st
( a,c // a9,c9 & b,c // b9,c9 )
then A11: Line (a,a9) is being_line by A4, AFF_1:def_3;
A12: a <> b by A1, AFF_1:7;
then A13: Line (a,b) c= X by A4, A5, A7, Th19;
A14: Line (a,b) // Line (a9,b9) by A2, A3, A12, AFF_1:37;
then consider Y being Subset of AS such that
A15: Line (a,b) c= Y and
A16: Line (a9,b9) c= Y and
A17: Y is being_plane by Th39;
A18: b in Line (a,b) by AFF_1:15;
A19: a9 in Line (a9,b9) by AFF_1:15;
then A20: Line (a,a9) c= Y by A4, A10, A9, A15, A16, A17, Th19;
A21: b9 in Line (a9,b9) by AFF_1:15;
A22: not b9 in X
proof
assume  b9 in X ; ::_thesis: contradiction
then  Line (a9,b9) c= X by A7, A21, A14, A13, Th23;
hence  contradiction by A10, A19; ::_thesis: verum
end;
then A23: Line (b,b9) is being_line by A5, AFF_1:def_3;
A24: b9 in Line (b,b9) by AFF_1:15;
A25: a in Line (a,a9) by AFF_1:15;
A26: a <> c by A1, AFF_1:7;
A27: b in Line (b,b9) by AFF_1:15;
A28: a9 in Line (a,a9) by AFF_1:15;
A29: Line (a,b) is being_line by A12, AFF_1:def_3;
A30: Line (a,a9) <> Line (b,b9)
proof
assume  Line (a,a9) = Line (b,b9) ; ::_thesis: contradiction
then  Line (a,a9) = Line (a,b) by A12, A9, A18, A29, A11, A25, A27, AFF_1:18;
hence  contradiction by A10, A13, A28; ::_thesis: verum
end;
A31: now__::_thesis:_(_Line_(a,a9)_//_Line_(b,b9)_implies_ex_c9_being_Element_of_AS_st_
(_a,c_//_a9,c9_&_b,c_//_b9,c9_)_)
set C = c * (Line (a,a9));
assume A32: Line (a,a9) // Line (b,b9) ; ::_thesis: ex c9 being Element of AS st
( a,c // a9,c9 & b,c // b9,c9 )
A33: c in c * (Line (a,a9)) by A11, Def3;
A34: Line (a,a9) <> c * (Line (a,a9))
proof
assume  Line (a,a9) = c * (Line (a,a9)) ; ::_thesis: contradiction
then  Line (a,a9) = Line (a,c) by A26, A11, A25, A33, AFF_1:57;
then  Line (a,a9) c= X by A4, A6, A7, A26, Th19;
hence  contradiction by A10, A28; ::_thesis: verum
end;
A35: Line (a,a9) // c * (Line (a,a9)) by A11, Def3;
then consider c9 being Element of AS such that
A36: c9 in c * (Line (a,a9)) and
A37: a,c // a9,c9 by A25, A28, A33, Lm2;
 c * (Line (a,a9)) is being_line by A11, Th27;
then  b,c // b9,c9 by A3, A8, A11, A23, A25, A28, A27, A24, A30, A32, A33, A35, A36, A37, A34, Th51;
hence  ex c9 being Element of AS st
( a,c // a9,c9 & b,c // b9,c9 ) by A37; ::_thesis: verum
end;
A38: a9 in Y by A19, A16;
A39: now__::_thesis:_(_ex_q_being_Element_of_AS_st_
(_q_in_Line_(a,a9)_&_q_in_Line_(b,b9)_)_implies_ex_c9_being_Element_of_AS_st_
(_a,c_//_a9,c9_&_b,c_//_b9,c9_)_)
given q being Element of AS such that A40: q in Line (a,a9) and
A41: q in Line (b,b9) ; ::_thesis: ex c9 being Element of AS st
( a,c // a9,c9 & b,c // b9,c9 )
A42: q <> a
proof
assume  q = a ; ::_thesis: contradiction
then  Line (a,b) = Line (b,b9) by A12, A9, A18, A29, A23, A27, A41, AFF_1:18;
hence  contradiction by A13, A22, A24; ::_thesis: verum
end;
A43: q <> b
proof
assume  q = b ; ::_thesis: contradiction
then  Line (a,b) = Line (a,a9) by A12, A9, A18, A29, A11, A25, A40, AFF_1:18;
hence  contradiction by A10, A13, A28; ::_thesis: verum
end;
set C = Line (q,c);
A44: c in Line (q,c) by AFF_1:15;
A45: Line (a,a9) <> Line (q,c)
proof
assume  Line (a,a9) = Line (q,c) ; ::_thesis: contradiction
then  Line (a,a9) = Line (a,c) by A26, A11, A25, A44, AFF_1:57;
then  Line (a,a9) c= X by A4, A6, A7, A26, Th19;
hence  contradiction by A10, A28; ::_thesis: verum
end;
 LIN q,a,a9 by A11, A25, A28, A40, AFF_1:21;
then consider c9 being Element of AS such that
A46: LIN q,c,c9 and
A47: a,c // a9,c9 by A42, Th1;
A48: q <> c by A1, A4, A5, A6, A7, A10, A9, A18, A15, A17, A38, A20, A40, Th25;
then A49: ( q in Line (q,c) & Line (q,c) is being_line ) by AFF_1:15, AFF_1:def_3;
then  c9 in Line (q,c) by A48, A44, A46, AFF_1:25;
then  b,c // b9,c9 by A3, A8, A11, A23, A25, A28, A27, A24, A30, A40, A41, A42, A43, A48, A44, A49, A47, A45, Th49;
hence  ex c9 being Element of AS st
( a,c // a9,c9 & b,c // b9,c9 ) by A47; ::_thesis: verum
end;
 Line (b,b9) c= Y by A5, A18, A21, A22, A15, A16, A17, Th19;
hence  ex c9 being Element of AS st
( a,c // a9,c9 & b,c // b9,c9 ) by A17, A11, A23, A20, A31, A39, Th22; ::_thesis: verum
end;
hence  ex c9 being Element of AS st
( a,c // a9,c9 & b,c // b9,c9 ) by A1, A3, A4, A5, A6, A7, Lm12; ::_thesis: verum
end;
hence  ex c9 being Element of AS st
( a,c // a9,c9 & b,c // b9,c9 ) by A1, Th53; ::_thesis: verum
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 ) ) )
proof
let AS be AffinSpace; ::_thesis: 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 ) ) )
let X, Y be Subset of AS; ::_thesis: ( X is being_plane & Y is being_plane implies ( 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 ) ) ) )
assume that
A1: X is being_plane and
A2: Y is being_plane ; ::_thesis: ( 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 ) ) )
A3: now__::_thesis:_(_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_)_)_implies_X_'||'_Y_)
given A, P, M, N being Subset of AS such that A4: not A // P and
A5: A c= X and
A6: P c= X and
A7: M c= Y and
A8: N c= Y and
A9: ( A // M or M // A ) and
A10: ( P // N or N // P ) ; ::_thesis: X '||' Y
A11: M is being_line by A9, AFF_1:36;
A12: not M // N
proof
assume  M // N ; ::_thesis: contradiction
then  P // M by A10, AFF_1:44;
hence  contradiction by A4, A9, AFF_1:44; ::_thesis: verum
end;
 N is being_line by A10, AFF_1:36;
then consider q being Element of AS such that
A13: q in M and
A14: q in N by A2, A7, A8, A11, A12, Th22;
A15: A is being_line by A9, AFF_1:36;
A16: P is being_line by A10, AFF_1:36;
then consider p being Element of AS such that
A17: p in A and
A18: p in P by A1, A4, A5, A6, A15, Th22;
now__::_thesis:_for_a_being_Element_of_AS
for_Z_being_Subset_of_AS_st_a_in_Y_&_Z_is_being_line_&_Z_c=_X_holds_
a_*_Z_c=_Y
let a be Element of AS; ::_thesis: for Z being Subset of AS st a in Y & Z is being_line & Z c= X holds
a * Z c= Y
let Z be Subset of AS; ::_thesis: ( a in Y & Z is being_line & Z c= X implies a * Z c= Y )
assume that
A19: a in Y and
A20: Z is being_line and
A21: Z c= X ; ::_thesis: a * Z c= Y
A22: a in a * Z by A20, Def3;
A23: Z // a * Z by A20, Def3;
A24: now__::_thesis:_(_Z_//_P_implies_a_*_Z_c=_Y_)
assume  Z // P ; ::_thesis: a * Z c= Y
then  Z // N by A10, AFF_1:44;
then  a * Z // N by A23, AFF_1:44;
hence  a * Z c= Y by A2, A8, A19, A22, Th23; ::_thesis: verum
end;
A25: now__::_thesis:_(_not_Z_//_A_&_not_Z_//_P_implies_a_*_Z_c=_Y_)
assume that
A26: not Z // A and
A27: not Z // P ; ::_thesis: a * Z c= Y
consider b being Element of AS such that
A28: p <> b and
A29: b in A by A15, AFF_1:20;
set Z1 = b * Z;
A30: b * Z is being_line by A20, Th27;
A31: not b * Z // P
proof
assume A32: b * Z // P ; ::_thesis: contradiction
 Z // b * Z by A20, Def3;
hence  contradiction by A27, A32, AFF_1:44; ::_thesis: verum
end;
A33: Z // b * Z by A20, Def3;
 b * Z c= X by A1, A5, A20, A21, A29, Th28;
then consider c being Element of AS such that
A34: c in b * Z and
A35: c in P by A1, A6, A16, A30, A31, Th22;
A36: b in b * Z by A20, Def3;
then A37: p <> c by A15, A17, A26, A28, A29, A30, A33, A34, AFF_1:18;
A38: A <> P by A4, A15, AFF_1:41;
A39: not LIN p,b,c
proof
assume  LIN p,b,c ; ::_thesis: contradiction
then  c in A by A15, A17, A28, A29, AFF_1:25;
hence  contradiction by A15, A16, A17, A18, A35, A37, A38, AFF_1:18; ::_thesis: verum
end;
then A40: b <> c by AFF_1:7;
consider b9 being Element of AS such that
A41: q <> b9 and
A42: b9 in M by A11, AFF_1:20;
 p,b // q,b9 by A9, A17, A13, A29, A42, AFF_1:39;
then consider c9 being Element of AS such that
A43: p,c // q,c9 and
A44: b,c // b9,c9 by A41, A39, Th54;
set Z2 = Line (b9,c9);
A45: ( b9 in Line (b9,c9) & c9 in Line (b9,c9) ) by AFF_1:15;
A46: b9 <> c9
proof
assume A47: b9 = c9 ; ::_thesis: contradiction
 q,b9 // M by A11, A13, A42, AFF_1:52;
then  p,c // M by A41, A43, A47, Th4;
then  p,c // A by A9, Th3;
then  c in A by A17, Th2;
hence  contradiction by A15, A16, A17, A18, A35, A37, A38, AFF_1:18; ::_thesis: verum
end;
then  Line (b9,c9) is being_line by AFF_1:def_3;
then  b * Z // Line (b9,c9) by A30, A36, A34, A44, A40, A46, A45, AFF_1:38;
then  Z // Line (b9,c9) by A33, AFF_1:44;
then A48: a * Z // Line (b9,c9) by A23, AFF_1:44;
 c9 in N by A10, A18, A14, A35, A37, A43, Th7;
then  Line (b9,c9) c= Y by A2, A7, A8, A42, A46, Th19;
hence  a * Z c= Y by A2, A19, A22, A48, Th23; ::_thesis: verum
end;
now__::_thesis:_(_Z_//_A_implies_a_*_Z_c=_Y_)
assume  Z // A ; ::_thesis: a * Z c= Y
then  Z // M by A9, AFF_1:44;
then  a * Z // M by A23, AFF_1:44;
hence  a * Z c= Y by A2, A7, A19, A22, Th23; ::_thesis: verum
end;
hence  a * Z c= Y by A24, A25; ::_thesis: verum
end;
hence  X '||' Y by Def4; ::_thesis: verum
end;
now__::_thesis:_(_X_'||'_Y_implies_ex_A,_P_being_Element_of_K24(_the_carrier_of_AS)_ex_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_)_)_)
consider a9, b9, c9 being Element of AS such that
A49: a9 in Y and
 b9 in Y and
 c9 in Y and
 not LIN a9,b9,c9 by A2, Th34;
assume A50: X '||' Y ; ::_thesis: ex A, P being Element of K24( the carrier of AS) ex 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 ) )
consider a, b, c being Element of AS such that
A51: a in X and
A52: b in X and
A53: c in X and
A54: not LIN a,b,c by A1, Th34;
set A = Line (a,b);
set P = Line (a,c);
A55: ( b in Line (a,b) & c in Line (a,c) ) by AFF_1:15;
A56: a <> c by A54, AFF_1:7;
then A57: Line (a,c) c= X by A1, A51, A53, Th19;
take A = Line (a,b); ::_thesis: ex P being Element of K24( the carrier of AS) ex 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 ) )
take P = Line (a,c); ::_thesis: ex 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 ) )
take M = a9 * A; ::_thesis: ex 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 ) )
take N = a9 * P; ::_thesis: ( 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 ) )
A58: a in A by AFF_1:15;
A59: a <> b by A54, AFF_1:7;
then A60: A is being_line by AFF_1:def_3;
A61: a in P by AFF_1:15;
A62: not A // P
proof
assume  A // P ; ::_thesis: contradiction
then  A = P by A58, A61, AFF_1:45;
hence  contradiction by A54, A58, A55, A60, AFF_1:21; ::_thesis: verum
end;
A63: P is being_line by A56, AFF_1:def_3;
 A c= X by A1, A51, A52, A59, Th19;
hence  ( 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 ) ) by A50, A60, A63, A49, A62, A57, Def3, Def4; ::_thesis: verum
end;
hence  ( 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 ) ) ) by A3; ::_thesis: verum
end;

theorem :: AFF_4:56
for AS being AffinSpace
for A, M, X being Subset of AS st A // M & M '||' X holds
A '||' X
proof
let AS be AffinSpace; ::_thesis: for A, M, X being Subset of AS st A // M & M '||' X holds
A '||' X
let A, M, X be Subset of AS; ::_thesis: ( A // M & M '||' X implies A '||' X )
assume that
A1: A // M and
A2: M '||' X ; ::_thesis: A '||' X
A3: M is being_line by A1, AFF_1:36;
A4: A is being_line by A1, AFF_1:36;
now__::_thesis:_for_a_being_Element_of_AS
for_C_being_Subset_of_AS_st_a_in_X_&_C_is_being_line_&_C_c=_A_holds_
a_*_C_c=_X
consider q, p being Element of AS such that
A5: q in A and
 p in A and
 q <> p by A4, AFF_1:19;
let a be Element of AS; ::_thesis: for C being Subset of AS st a in X & C is being_line & C c= A holds
a * C c= X
let C be Subset of AS; ::_thesis: ( a in X & C is being_line & C c= A implies a * C c= X )
assume that
A6: a in X and
A7: ( C is being_line & C c= A ) ; ::_thesis: a * C c= X
A8: a * A = a * (q * M) by A1, A3, A5, Def3
.= a * M by A3, Th31 ;
 C = A by A4, A7, Th33;
hence  a * C c= X by A2, A3, A6, A8, Def4; ::_thesis: verum
end;
hence  A '||' X by Def4; ::_thesis: verum
end;

theorem Th57: :: AFF_4:57
for AS being AffinSpace
for X being Subset of AS st X is being_plane holds
X '||' X
proof
let AS be AffinSpace; ::_thesis: for X being Subset of AS st X is being_plane holds
X '||' X
let X be Subset of AS; ::_thesis: ( X is being_plane implies X '||' X )
assume  X is being_plane ; ::_thesis: X '||' X
then  for a being Element of AS
for A being Subset of AS st a in X & A is being_line & A c= X holds
a * A c= X by Th28;
hence  X '||' X by Def4; ::_thesis: verum
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
proof
let AS be AffinSpace; ::_thesis: for X, Y being Subset of AS st X is being_plane & Y is being_plane & X '||' Y holds
Y '||' X
let X, Y be Subset of AS; ::_thesis: ( X is being_plane & Y is being_plane & X '||' Y implies Y '||' X )
assume that
A1: ( X is being_plane & Y is being_plane ) and
A2: X '||' Y ; ::_thesis: Y '||' X
consider A, P, M, N being Subset of AS such that
A3: not A // P and
A4: ( A c= X & P c= X & M c= Y & N c= Y ) and
A5: ( A // M or M // A ) and
A6: ( P // N or N // P ) by A1, A2, Th55;
 not M // N
proof
assume  M // N ; ::_thesis: contradiction
then  A // N by A5, AFF_1:44;
hence  contradiction by A3, A6, AFF_1:44; ::_thesis: verum
end;
hence  Y '||' X by A1, A4, A5, A6, Th55; ::_thesis: verum
end;

theorem Th59: :: AFF_4:59
for AS being AffinSpace
for X being Subset of AS st X is being_plane holds
X <> {}
proof
let AS be AffinSpace; ::_thesis: for X being Subset of AS st X is being_plane holds
X <> {}
let X be Subset of AS; ::_thesis: ( X is being_plane implies X <> {} )
assume  X is being_plane ; ::_thesis: X <> {}
then  ex a, b, c being Element of AS st
( a in X & b in X & c in X & not LIN a,b,c ) by Th34;
hence  X <> {} ; ::_thesis: verum
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
proof
let AS be AffinSpace; ::_thesis: for X, Y, Z being Subset of AS st X '||' Y & Y '||' Z & Y <> {} holds
X '||' Z
let X, Y, Z be Subset of AS; ::_thesis: ( X '||' Y & Y '||' Z & Y <> {} implies X '||' Z )
assume that
A1: X '||' Y and
A2: Y '||' Z and
A3: Y <> {} ; ::_thesis: X '||' Z
set x = the Element of Y;
reconsider p = the Element of Y as Element of AS by A3, Lm1;
now__::_thesis:_for_a_being_Element_of_AS
for_A_being_Subset_of_AS_st_a_in_Z_&_A_is_being_line_&_A_c=_X_holds_
a_*_A_c=_Z
let a be Element of AS; ::_thesis: for A being Subset of AS st a in Z & A is being_line & A c= X holds
a * A c= Z
let A be Subset of AS; ::_thesis: ( a in Z & A is being_line & A c= X implies a * A c= Z )
assume that
A4: a in Z and
A5: A is being_line and
A6: A c= X ; ::_thesis: a * A c= Z
 ( p * A c= Y & p * A is being_line ) by A1, A3, A5, A6, Def4, Th27;
then  a * (p * A) c= Z by A2, A4, Def4;
hence  a * A c= Z by A5, Th31; ::_thesis: verum
end;
hence  X '||' Z by Def4; ::_thesis: verum
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
proof
let AS be AffinSpace; ::_thesis: 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
let X, Y, Z be Subset of AS; ::_thesis: ( 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 ) ) implies X '||' Z )
assume that
A1: X is being_plane and
A2: Y is being_plane and
A3: ( Z is being_plane & ( ( X '||' Y & Y '||' Z ) or ( X '||' Y & Z '||' Y ) or ( Y '||' X & Y '||' Z ) or ( Y '||' X & Z '||' Y ) ) ) ; ::_thesis: X '||' Z
 ( X '||' Y & Y '||' Z ) by A1, A2, A3, Th58;
hence  X '||' Z by A2, Th59, Th60; ::_thesis: verum
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
let AS be AffinSpace; ::_thesis: 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 )
let X, Y be Subset of AS; ::_thesis: ( X is being_plane & Y is being_plane & X '||' Y & X <> Y implies for a being Element of AS holds
( not a in X or not a in Y ) )
assume that
A1: X is being_plane and
A2: Y is being_plane and
A3: X '||' Y and
A4: X <> Y ; ::_thesis: for a being Element of AS holds
( not a in X or not a in Y )
assume  ex a being Element of AS st
( a in X & a in Y ) ; ::_thesis: contradiction
then consider a being Element of AS such that
A5: a in X and
A6: a in Y ;
consider b, c being Element of AS such that
A7: b in X and
A8: c in X and
A9: not LIN a,b,c by A1, Lm9;
set M = Line (a,b);
set N = Line (a,c);
A10: a <> c by A9, AFF_1:7;
then A11: Line (a,c) c= X by A1, A5, A8, Th19;
A12: a <> b by A9, AFF_1:7;
then A13: Line (a,b) is being_line by AFF_1:def_3;
A14: Line (a,b) <> Line (a,c)
proof
assume  Line (a,b) = Line (a,c) ; ::_thesis: contradiction
then A15: c in Line (a,b) by AFF_1:15;
 ( a in Line (a,b) & b in Line (a,b) ) by AFF_1:15;
hence  contradiction by A9, A13, A15, AFF_1:21; ::_thesis: verum
end;
A16: Line (a,c) is being_line by A10, AFF_1:def_3;
then  ( a in Line (a,c) & a * (Line (a,c)) c= Y ) by A3, A6, A11, Def4, AFF_1:15;
then A17: Line (a,c) c= Y by A16, Lm8;
A18: Line (a,b) c= X by A1, A5, A7, A12, Th19;
then  ( a in Line (a,b) & a * (Line (a,b)) c= Y ) by A3, A6, A13, Def4, AFF_1:15;
then  Line (a,b) c= Y by A13, Lm8;
hence  contradiction by A1, A2, A4, A13, A16, A18, A11, A17, A14, Th26; ::_thesis: verum
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;

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
proof
let AS be AffinSpace; ::_thesis: 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
let a, b, c, d be Element of AS; ::_thesis: 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
let X, Y, Z be Subset of AS; ::_thesis: ( 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 implies a,b // c,d )
assume that
A1: X is being_plane and
A2: Y is being_plane and
A3: Z is being_plane and
A4: X '||' Y and
A5: X <> Y and
A6: a in X /\ Z and
A7: b in X /\ Z and
A8: c in Y /\ Z and
A9: d in Y /\ Z ; ::_thesis: a,b // c,d
A10: c in Z by A8, XBOOLE_0:def_4;
A11: ( a in X & a in Z ) by A6, XBOOLE_0:def_4;
then A12: Z <> Y by A1, A2, A4, A5, Lm13;
A13: c in Y by A8, XBOOLE_0:def_4;
then A14: Z <> X by A1, A2, A4, A5, A10, Lm13;
set A = X /\ Z;
set C = Y /\ Z;
A15: ( b in X & b in Z ) by A7, XBOOLE_0:def_4;
A16: ( d in Y & d in Z ) by A9, XBOOLE_0:def_4;
now__::_thesis:_(_a_<>_b_&_c_<>_d_implies_a,b_//_c,d_)
A17: ( Y /\ Z c= Y & Y /\ Z c= Z ) by XBOOLE_1:17;
set K = c * (X /\ Z);
assume that
A18: a <> b and
A19: c <> d ; ::_thesis: a,b // c,d
A20: X /\ Z is being_line by A1, A3, A11, A15, A14, A18, Th24;
then A21: X /\ Z // c * (X /\ Z) by Def3;
 X /\ Z c= X by XBOOLE_1:17;
then A22: c * (X /\ Z) c= Y by A4, A13, A20, Def4;
A23: c * (X /\ Z) c= Z by A3, A10, A20, Th28, XBOOLE_1:17;
 ( Y /\ Z is being_line & c * (X /\ Z) is being_line ) by A1, A2, A3, A11, A15, A13, A10, A16, A12, A14, A18, A19, Th24, Th27;
then  c * (X /\ Z) = Y /\ Z by A2, A3, A12, A17, A23, A22, Th26;
hence  a,b // c,d by A6, A7, A8, A9, A21, AFF_1:39; ::_thesis: verum
end;
hence  a,b // c,d by AFF_1:3; ::_thesis: verum
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
proof
let AS be AffinSpace; ::_thesis: 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
let a, b, c, d be Element of AS; ::_thesis: 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
let X, Y, Z be Subset of AS; ::_thesis: ( 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 implies X /\ Z // Y /\ Z )
assume that
A1: X is being_plane and
A2: Y is being_plane and
A3: Z is being_plane and
A4: X '||' Y and
A5: a in X /\ Z and
A6: b in X /\ Z and
A7: c in Y /\ Z and
A8: d in Y /\ Z and
A9: X <> Y and
A10: a <> b and
A11: c <> d ; ::_thesis: X /\ Z // Y /\ Z
A12: ( d in Y & d in Z ) by A8, XBOOLE_0:def_4;
set A = X /\ Z;
set C = Y /\ Z;
A13: ( c in Y & c in Z ) by A7, XBOOLE_0:def_4;
A14: ( a in X & a in Z ) by A5, XBOOLE_0:def_4;
then  Z <> Y by A1, A2, A4, A9, Lm13;
then A15: Y /\ Z is being_line by A2, A3, A11, A13, A12, Th24;
A16: ( b in X & b in Z ) by A6, XBOOLE_0:def_4;
 Z <> X by A1, A2, A4, A9, A13, Lm13;
then A17: X /\ Z is being_line by A1, A3, A10, A14, A16, Th24;
 a,b // c,d by A1, A2, A3, A4, A5, A6, A7, A8, A9, Th63;
hence  X /\ Z // Y /\ Z by A5, A6, A7, A8, A10, A11, A17, A15, AFF_1:38; ::_thesis: verum
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 )
proof
let AS be AffinSpace; ::_thesis: 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 )
let a be Element of AS; ::_thesis: 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 )
let X be Subset of AS; ::_thesis: ( X is being_plane implies ex Y being Subset of AS st
( a in Y & X '||' Y & Y is being_plane ) )
assume A1: X is being_plane ; ::_thesis: ex Y being Subset of AS st
( a in Y & X '||' Y & Y is being_plane )
then consider p, q, r being Element of AS such that
A2: p in X and
A3: q in X and
A4: r in X and
A5: not LIN p,q,r by Th34;
set M = Line (p,q);
set N = Line (p,r);
A6: p <> r by A5, AFF_1:7;
then A7: Line (p,r) c= X by A1, A2, A4, Th19;
set M9 = a * (Line (p,q));
set N9 = a * (Line (p,r));
A8: p <> q by A5, AFF_1:7;
then A9: Line (p,q) is being_line by AFF_1:def_3;
then A10: a * (Line (p,q)) is being_line by Th27;
A11: ( p in Line (p,r) & r in Line (p,r) ) by AFF_1:15;
A12: p in Line (p,q) by AFF_1:15;
A13: q in Line (p,q) by AFF_1:15;
A14: not Line (p,q) // Line (p,r)
proof
assume  Line (p,q) // Line (p,r) ; ::_thesis: contradiction
then  r in Line (p,q) by A12, A11, AFF_1:45;
hence  contradiction by A5, A12, A13, A9, AFF_1:21; ::_thesis: verum
end;
A15: Line (p,r) is being_line by A6, AFF_1:def_3;
then A16: Line (p,r) // a * (Line (p,r)) by Def3;
A17: Line (p,q) // a * (Line (p,q)) by A9, Def3;
A18: a in a * (Line (p,q)) by A9, Def3;
 ( a * (Line (p,r)) is being_line & a in a * (Line (p,r)) ) by A15, Def3, Th27;
then consider Y being Subset of AS such that
A19: a * (Line (p,q)) c= Y and
A20: a * (Line (p,r)) c= Y and
A21: Y is being_plane by A10, A18, Th38;
 Line (p,q) c= X by A1, A2, A3, A8, Th19;
then  X '||' Y by A1, A17, A16, A19, A20, A21, A7, A14, Th55;
hence  ex Y being Subset of AS st
( a in Y & X '||' Y & Y is being_plane ) by A18, A19, A21; ::_thesis: verum
end;

definition
let AS be AffinSpace;
let a be Element of AS;
let X be Subset of AS;
assume B1: X is being_plane ;
funca + X ->  Subset of AS means :Def6: :: AFF_4:def 6
( a in it & X '||' it & it is being_plane );
existence
 ex b1 being Subset of AS st
( a in b1 & X '||' b1 & b1 is being_plane ) by B1, Th65;
uniqueness
 for b1, b2 being Subset of AS st a in b1 & X '||' b1 & b1 is being_plane & a in b2 & X '||' b2 & b2 is being_plane holds
b1 = b2
proof
let Y1, Y2 be Subset of AS; ::_thesis: ( a in Y1 & X '||' Y1 & Y1 is being_plane & a in Y2 & X '||' Y2 & Y2 is being_plane implies Y1 = Y2 )
assume that
A1: a in Y1 and
A2: X '||' Y1 and
A3: Y1 is being_plane and
A4: a in Y2 and
A5: X '||' Y2 and
A6: Y2 is being_plane ; ::_thesis: Y1 = Y2
 Y1 '||' Y2 by B1, A2, A3, A5, A6, Th61;
hence  Y1 = Y2 by A1, A3, A4, A6, Lm13; ::_thesis: verum
end;
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 b4 being Subset of AS holds
( b4 = a + X iff ( a in b4 & X '||' b4 & b4 is being_plane ) );

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 )
proof
let AS be AffinSpace; ::_thesis: 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 )
let a be Element of AS; ::_thesis: for X being Subset of AS st X is being_plane holds
( a in X iff a + X = X )
let X be Subset of AS; ::_thesis: ( X is being_plane implies ( a in X iff a + X = X ) )
assume A1: X is being_plane ; ::_thesis: ( a in X iff a + X = X )
now__::_thesis:_(_a_in_X_implies_a_+_X_=_X_)
assume A2: a in X ; ::_thesis: a + X = X
 X '||' X by A1, Th57;
hence  a + X = X by A1, A2, Def6; ::_thesis: verum
end;
hence  ( a in X iff a + X = X ) by A1, Def6; ::_thesis: verum
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)
proof
let AS be AffinSpace; ::_thesis: for a, q being Element of AS
for X being Subset of AS st X is being_plane holds
a + X = a + (q + X)
let a, q be Element of AS; ::_thesis: for X being Subset of AS st X is being_plane holds
a + X = a + (q + X)
let X be Subset of AS; ::_thesis: ( X is being_plane implies a + X = a + (q + X) )
assume A1: X is being_plane ; ::_thesis: a + X = a + (q + X)
then A2: a in a + X by Def6;
A3: a + X is being_plane by A1, Def6;
A4: q + X is being_plane by A1, Def6;
then A5: q + X '||' a + (q + X) by Def6;
A6: a in a + (q + X) by A4, Def6;
A7: a + (q + X) is being_plane by A4, Def6;
 ( X '||' q + X & X '||' a + X ) by A1, Def6;
then  a + X '||' q + X by A1, A4, A3, Th61;
then  a + X '||' a + (q + X) by A4, A5, A3, A7, Th61;
hence  a + X = a + (q + X) by A2, A6, A3, A7, Lm13; ::_thesis: verum
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
proof
let AS be AffinSpace; ::_thesis: 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
let a be Element of AS; ::_thesis: for A, X being Subset of AS st A is being_line & X is being_plane & A '||' X holds
a * A c= a + X
let A, X be Subset of AS; ::_thesis: ( A is being_line & X is being_plane & A '||' X implies a * A c= a + X )
assume that
A1: A is being_line and
A2: X is being_plane and
A3: A '||' X ; ::_thesis: a * A c= a + X
A4: ( X '||' a + X & a in a + X ) by A2, Def6;
consider N being Subset of AS such that
A5: N c= X and
A6: ( A // N or N // A ) by A1, A2, A3, Th41;
 ( a * A = a * N & N is being_line ) by A6, Th32, AFF_1:36;
hence  a * A c= a + X by A5, A4, Def4; ::_thesis: verum
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
proof
let AS be AffinSpace; ::_thesis: 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
let a be Element of AS; ::_thesis: for X, Y being Subset of AS st X is being_plane & Y is being_plane & X '||' Y holds
a + X = a + Y
let X, Y be Subset of AS; ::_thesis: ( X is being_plane & Y is being_plane & X '||' Y implies a + X = a + Y )
assume that
A1: X is being_plane and
A2: Y is being_plane and
A3: X '||' Y ; ::_thesis: a + X = a + Y
A4: a + X is being_plane by A1, Def6;
A5: ( a in a + X & a in a + Y ) by A1, A2, Def6;
A6: a + Y is being_plane by A2, Def6;
 X '||' a + X by A1, Def6;
then A7: a + X '||' Y by A1, A2, A3, A4, Th61;
 Y '||' a + Y by A2, Def6;
then  a + X '||' a + Y by A2, A4, A6, A7, Th61;
hence  a + X = a + Y by A5, A4, A6, Lm13; ::_thesis: verum
end;