:: AFF_4 semantic presentation

begin

theorem :: AFF_4:1
for AS being ( ( V46() AffinSpace-like ) ( non empty V46() AffinSpace-like ) AffinSpace)
for p, a, a9, b being ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) st ( LIN p : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ,a9 : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) or LIN p : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ,a9 : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ) & p : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) <> a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) holds
ex b9 being ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) st
( LIN p : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) // a9 : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ) ;

theorem :: AFF_4:2
for AS being ( ( V46() AffinSpace-like ) ( non empty V46() AffinSpace-like ) AffinSpace)
for a, b being ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) )
for A being ( ( ) ( ) Subset of ) st ( a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) // A : ( ( ) ( ) Subset of ) or b : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) // A : ( ( ) ( ) Subset of ) ) & a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in A : ( ( ) ( ) Subset of ) holds
b : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in A : ( ( ) ( ) Subset of ) ;

theorem :: AFF_4:3
for AS being ( ( V46() AffinSpace-like ) ( non empty V46() AffinSpace-like ) AffinSpace)
for a, b being ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) )
for A, K being ( ( ) ( ) Subset of ) st ( a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) // A : ( ( ) ( ) Subset of ) or b : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) // A : ( ( ) ( ) Subset of ) ) & A : ( ( ) ( ) Subset of ) // K : ( ( ) ( ) Subset of ) holds
( a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) // K : ( ( ) ( ) Subset of ) & b : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) // K : ( ( ) ( ) Subset of ) ) ;

theorem :: AFF_4:4
for AS being ( ( V46() AffinSpace-like ) ( non empty V46() AffinSpace-like ) AffinSpace)
for a, b, c, d being ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) )
for A being ( ( ) ( ) Subset of ) st ( a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) // A : ( ( ) ( ) Subset of ) or b : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) // A : ( ( ) ( ) Subset of ) ) & ( a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) or c : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) // a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ) & a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) <> b : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) holds
( c : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) // A : ( ( ) ( ) Subset of ) & d : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) // A : ( ( ) ( ) Subset of ) ) ;

theorem :: AFF_4:5
for AS being ( ( V46() AffinSpace-like ) ( non empty V46() AffinSpace-like ) AffinSpace)
for a, b being ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) )
for M, N being ( ( ) ( ) Subset of ) st ( a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) // M : ( ( ) ( ) Subset of ) or b : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) // M : ( ( ) ( ) Subset of ) ) & ( a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) // N : ( ( ) ( ) Subset of ) or b : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) // N : ( ( ) ( ) Subset of ) ) & a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) <> b : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) holds
M : ( ( ) ( ) Subset of ) // N : ( ( ) ( ) Subset of ) ;

theorem :: AFF_4:6
for AS being ( ( V46() AffinSpace-like ) ( non empty V46() AffinSpace-like ) AffinSpace)
for a, b, c, d being ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) )
for M being ( ( ) ( ) Subset of ) st ( a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) // M : ( ( ) ( ) Subset of ) or b : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) // M : ( ( ) ( ) Subset of ) ) & ( c : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) // M : ( ( ) ( ) Subset of ) or d : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) // M : ( ( ) ( ) Subset of ) ) holds
a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ;

theorem :: AFF_4:7
for AS being ( ( V46() AffinSpace-like ) ( non empty V46() AffinSpace-like ) AffinSpace)
for a, b, c, d being ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) )
for A, C being ( ( ) ( ) Subset of ) st ( A : ( ( ) ( ) Subset of ) // C : ( ( ) ( ) Subset of ) or C : ( ( ) ( ) Subset of ) // A : ( ( ) ( ) Subset of ) ) & a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) <> b : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) & ( a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) or c : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) // a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ) & a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in A : ( ( ) ( ) Subset of ) & b : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in A : ( ( ) ( ) Subset of ) & c : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in C : ( ( ) ( ) Subset of ) holds
d : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in C : ( ( ) ( ) Subset of ) ;

theorem :: AFF_4:8
for AS being ( ( V46() AffinSpace-like ) ( non empty V46() AffinSpace-like ) AffinSpace)
for q, a, b, b9, a9 being ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) )
for M, N being ( ( ) ( ) Subset of ) st q : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in M : ( ( ) ( ) Subset of ) & q : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in N : ( ( ) ( ) Subset of ) & a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in M : ( ( ) ( ) Subset of ) & b : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in N : ( ( ) ( ) Subset of ) & b9 : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in N : ( ( ) ( ) Subset of ) & q : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) <> a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) & q : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) <> b : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) & M : ( ( ) ( ) Subset of ) <> N : ( ( ) ( ) Subset of ) & ( a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) // a9 : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) or b : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) // b9 : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ,a9 : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ) & M : ( ( ) ( ) Subset of ) is being_line & N : ( ( ) ( ) Subset of ) is being_line & q : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) = a9 : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) holds
q : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) = b9 : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ;

theorem :: AFF_4:9
for AS being ( ( V46() AffinSpace-like ) ( non empty V46() AffinSpace-like ) AffinSpace)
for q, a, a9, b, b9 being ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) )
for M, N being ( ( ) ( ) Subset of ) st q : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in M : ( ( ) ( ) Subset of ) & q : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in N : ( ( ) ( ) Subset of ) & a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in M : ( ( ) ( ) Subset of ) & a9 : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in M : ( ( ) ( ) Subset of ) & b : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in N : ( ( ) ( ) Subset of ) & b9 : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in N : ( ( ) ( ) Subset of ) & q : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) <> a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) & q : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) <> b : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) & M : ( ( ) ( ) Subset of ) <> N : ( ( ) ( ) Subset of ) & ( a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) // a9 : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) or b : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) // b9 : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ,a9 : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ) & M : ( ( ) ( ) Subset of ) is being_line & N : ( ( ) ( ) Subset of ) is being_line & a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) = a9 : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) holds
b : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) = b9 : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ;

theorem :: AFF_4:10
for AS being ( ( V46() AffinSpace-like ) ( non empty V46() AffinSpace-like ) AffinSpace)
for a, b, b9, a9 being ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) )
for M, N being ( ( ) ( ) Subset of ) st ( M : ( ( ) ( ) Subset of ) // N : ( ( ) ( ) Subset of ) or N : ( ( ) ( ) Subset of ) // M : ( ( ) ( ) Subset of ) ) & a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in M : ( ( ) ( ) Subset of ) & b : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in N : ( ( ) ( ) Subset of ) & b9 : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in N : ( ( ) ( ) Subset of ) & M : ( ( ) ( ) Subset of ) <> N : ( ( ) ( ) Subset of ) & ( a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) // a9 : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) or b : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) // b9 : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ,a9 : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ) & a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) = a9 : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) holds
b : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) = b9 : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ;

theorem :: AFF_4:11
for AS being ( ( V46() AffinSpace-like ) ( non empty V46() AffinSpace-like ) AffinSpace)
for a, b being ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ex A being ( ( ) ( ) Subset of ) st
( a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in A : ( ( ) ( ) Subset of ) & b : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in A : ( ( ) ( ) Subset of ) & A : ( ( ) ( ) Subset of ) is being_line ) ;

theorem :: AFF_4:12
for AS being ( ( V46() AffinSpace-like ) ( non empty V46() AffinSpace-like ) AffinSpace)
for A being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) is being_line holds
ex q being ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) st not q : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in A : ( ( ) ( ) Subset of ) ;

definition
let AS be ( ( V46() AffinSpace-like ) ( non empty V46() AffinSpace-like ) AffinSpace) ;
let K, P be ( ( ) ( ) Subset of ) ;
func Plane (K,P) -> ( ( ) ( ) Subset of ) equals :: AFF_4:def 1
 { a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) where a is ( ( ) ( ) Element of ( ( ) ( ) set ) ) : ex b being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st
( a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) // K : ( ( ) ( ) Element of K24(K25(K25(AS : ( ( ) ( ) AffinStruct ) ,AS : ( ( ) ( ) AffinStruct ) ) : ( ( ) ( ) set ) ,K25(AS : ( ( ) ( ) AffinStruct ) ,AS : ( ( ) ( ) AffinStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) & b : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in P : ( ( ) ( ) Element of AS : ( ( ) ( ) AffinStruct ) ) ) } ;
end;

definition
let AS be ( ( V46() AffinSpace-like ) ( non empty V46() AffinSpace-like ) AffinSpace) ;
let X be ( ( ) ( ) Subset of ) ;
attr X is being_plane means :: AFF_4:def 2
 ex K, P being ( ( ) ( ) Subset of ) st
( K : ( ( ) ( ) Subset of ) is being_line & P : ( ( ) ( ) Subset of ) is being_line & not K : ( ( ) ( ) Subset of ) // P : ( ( ) ( ) Subset of ) & X : ( ( ) ( ) Element of K24(K25(K25(AS : ( ( ) ( ) AffinStruct ) ,AS : ( ( ) ( ) AffinStruct ) ) : ( ( ) ( ) set ) ,K25(AS : ( ( ) ( ) AffinStruct ) ,AS : ( ( ) ( ) AffinStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = Plane (K : ( ( ) ( ) Subset of ) ,P : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Subset of ) );
end;

theorem :: AFF_4:13
for AS being ( ( V46() AffinSpace-like ) ( non empty V46() AffinSpace-like ) AffinSpace)
for K, P being ( ( ) ( ) Subset of ) st not K : ( ( ) ( ) Subset of ) is being_line holds
Plane (K : ( ( ) ( ) Subset of ) ,P : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Subset of ) = {} : ( ( ) ( empty ) set ) ;

theorem :: AFF_4:14
for AS being ( ( V46() AffinSpace-like ) ( non empty V46() AffinSpace-like ) AffinSpace)
for K, P being ( ( ) ( ) Subset of ) st K : ( ( ) ( ) Subset of ) is being_line holds
P : ( ( ) ( ) Subset of ) c= Plane (K : ( ( ) ( ) Subset of ) ,P : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Subset of ) ;

theorem :: AFF_4:15
for AS being ( ( V46() AffinSpace-like ) ( non empty V46() AffinSpace-like ) AffinSpace)
for K, P being ( ( ) ( ) Subset of ) st K : ( ( ) ( ) Subset of ) // P : ( ( ) ( ) Subset of ) holds
Plane (K : ( ( ) ( ) Subset of ) ,P : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Subset of ) = P : ( ( ) ( ) Subset of ) ;

theorem :: AFF_4:16
for AS being ( ( V46() AffinSpace-like ) ( non empty V46() AffinSpace-like ) AffinSpace)
for K, M, P being ( ( ) ( ) Subset of ) st K : ( ( ) ( ) Subset of ) // M : ( ( ) ( ) Subset of ) holds
Plane (K : ( ( ) ( ) Subset of ) ,P : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Subset of ) = Plane (M : ( ( ) ( ) Subset of ) ,P : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Subset of ) ;

theorem :: AFF_4:17
for AS being ( ( V46() AffinSpace-like ) ( non empty V46() AffinSpace-like ) AffinSpace)
for p, a, b, a9, b9 being ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) )
for M, N, P, Q being ( ( ) ( ) Subset of ) st p : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in M : ( ( ) ( ) Subset of ) & a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in M : ( ( ) ( ) Subset of ) & b : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in M : ( ( ) ( ) Subset of ) & p : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in N : ( ( ) ( ) Subset of ) & a9 : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in N : ( ( ) ( ) Subset of ) & b9 : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in N : ( ( ) ( ) Subset of ) & not p : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in P : ( ( ) ( ) Subset of ) & not p : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in Q : ( ( ) ( ) Subset of ) & M : ( ( ) ( ) Subset of ) <> N : ( ( ) ( ) Subset of ) & a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in P : ( ( ) ( ) Subset of ) & a9 : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in P : ( ( ) ( ) Subset of ) & b : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in Q : ( ( ) ( ) Subset of ) & b9 : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in Q : ( ( ) ( ) Subset of ) & M : ( ( ) ( ) Subset of ) is being_line & N : ( ( ) ( ) Subset of ) is being_line & P : ( ( ) ( ) Subset of ) is being_line & Q : ( ( ) ( ) Subset of ) is being_line & not P : ( ( ) ( ) Subset of ) // Q : ( ( ) ( ) Subset of ) holds
ex q being ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) st
( q : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in P : ( ( ) ( ) Subset of ) & q : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in Q : ( ( ) ( ) Subset of ) ) ;

theorem :: AFF_4:18
for AS being ( ( V46() AffinSpace-like ) ( non empty V46() AffinSpace-like ) AffinSpace)
for a, b, a9, b9 being ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) )
for M, N, P, Q being ( ( ) ( ) Subset of ) st a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in M : ( ( ) ( ) Subset of ) & b : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in M : ( ( ) ( ) Subset of ) & a9 : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in N : ( ( ) ( ) Subset of ) & b9 : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in N : ( ( ) ( ) Subset of ) & a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in P : ( ( ) ( ) Subset of ) & a9 : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in P : ( ( ) ( ) Subset of ) & b : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in Q : ( ( ) ( ) Subset of ) & b9 : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in Q : ( ( ) ( ) Subset of ) & M : ( ( ) ( ) Subset of ) <> N : ( ( ) ( ) Subset of ) & M : ( ( ) ( ) Subset of ) // N : ( ( ) ( ) Subset of ) & P : ( ( ) ( ) Subset of ) is being_line & Q : ( ( ) ( ) Subset of ) is being_line & not P : ( ( ) ( ) Subset of ) // Q : ( ( ) ( ) Subset of ) holds
ex q being ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) st
( q : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in P : ( ( ) ( ) Subset of ) & q : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in Q : ( ( ) ( ) Subset of ) ) ;

theorem :: AFF_4:19
for AS being ( ( V46() AffinSpace-like ) ( non empty V46() AffinSpace-like ) AffinSpace)
for a, b being ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) )
for X being ( ( ) ( ) Subset of ) st X : ( ( ) ( ) Subset of ) is being_plane & a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in X : ( ( ) ( ) Subset of ) & b : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in X : ( ( ) ( ) Subset of ) & a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) <> b : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) holds
Line (a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ) : ( ( ) ( ) Element of K24( the carrier of b1 : ( ( V46() AffinSpace-like ) ( non empty V46() AffinSpace-like ) AffinSpace) : ( ( ) ( non empty V5() ) set ) ) : ( ( ) ( ) set ) ) c= X : ( ( ) ( ) Subset of ) ;

theorem :: AFF_4:20
for AS being ( ( V46() AffinSpace-like ) ( non empty V46() AffinSpace-like ) AffinSpace)
for K, P, Q being ( ( ) ( ) Subset of ) st K : ( ( ) ( ) Subset of ) is being_line & P : ( ( ) ( ) Subset of ) is being_line & Q : ( ( ) ( ) Subset of ) is being_line & not K : ( ( ) ( ) Subset of ) // Q : ( ( ) ( ) Subset of ) & Q : ( ( ) ( ) Subset of ) c= Plane (K : ( ( ) ( ) Subset of ) ,P : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Subset of ) holds
Plane (K : ( ( ) ( ) Subset of ) ,Q : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Subset of ) = Plane (K : ( ( ) ( ) Subset of ) ,P : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Subset of ) ;

theorem :: AFF_4:21
for AS being ( ( V46() AffinSpace-like ) ( non empty V46() AffinSpace-like ) AffinSpace)
for K, P, Q being ( ( ) ( ) Subset of ) st K : ( ( ) ( ) Subset of ) is being_line & P : ( ( ) ( ) Subset of ) is being_line & Q : ( ( ) ( ) Subset of ) is being_line & Q : ( ( ) ( ) Subset of ) c= Plane (K : ( ( ) ( ) Subset of ) ,P : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Subset of ) & not P : ( ( ) ( ) Subset of ) // Q : ( ( ) ( ) Subset of ) holds
ex q being ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) st
( q : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in P : ( ( ) ( ) Subset of ) & q : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in Q : ( ( ) ( ) Subset of ) ) ;

theorem :: AFF_4:22
for AS being ( ( V46() AffinSpace-like ) ( non empty V46() AffinSpace-like ) AffinSpace)
for X, M, N being ( ( ) ( ) Subset of ) st X : ( ( ) ( ) Subset of ) is being_plane & M : ( ( ) ( ) Subset of ) is being_line & N : ( ( ) ( ) Subset of ) is being_line & M : ( ( ) ( ) Subset of ) c= X : ( ( ) ( ) Subset of ) & N : ( ( ) ( ) Subset of ) c= X : ( ( ) ( ) Subset of ) & not M : ( ( ) ( ) Subset of ) // N : ( ( ) ( ) Subset of ) holds
ex q being ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) st
( q : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in M : ( ( ) ( ) Subset of ) & q : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in N : ( ( ) ( ) Subset of ) ) ;

theorem :: AFF_4:23
for AS being ( ( V46() AffinSpace-like ) ( non empty V46() AffinSpace-like ) AffinSpace)
for a being ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) )
for X, M, N being ( ( ) ( ) Subset of ) st X : ( ( ) ( ) Subset of ) is being_plane & a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in X : ( ( ) ( ) Subset of ) & M : ( ( ) ( ) Subset of ) c= X : ( ( ) ( ) Subset of ) & a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in N : ( ( ) ( ) Subset of ) & ( M : ( ( ) ( ) Subset of ) // N : ( ( ) ( ) Subset of ) or N : ( ( ) ( ) Subset of ) // M : ( ( ) ( ) Subset of ) ) holds
N : ( ( ) ( ) Subset of ) c= X : ( ( ) ( ) Subset of ) ;

theorem :: AFF_4:24
for AS being ( ( V46() AffinSpace-like ) ( non empty V46() AffinSpace-like ) AffinSpace)
for a, b being ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) )
for X, Y being ( ( ) ( ) Subset of ) st X : ( ( ) ( ) Subset of ) is being_plane & Y : ( ( ) ( ) Subset of ) is being_plane & a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in X : ( ( ) ( ) Subset of ) & b : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in X : ( ( ) ( ) Subset of ) & a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in Y : ( ( ) ( ) Subset of ) & b : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in Y : ( ( ) ( ) Subset of ) & X : ( ( ) ( ) Subset of ) <> Y : ( ( ) ( ) Subset of ) & a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) <> b : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) holds
X : ( ( ) ( ) Subset of ) /\ Y : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K24( the carrier of b1 : ( ( V46() AffinSpace-like ) ( non empty V46() AffinSpace-like ) AffinSpace) : ( ( ) ( non empty V5() ) set ) ) : ( ( ) ( ) set ) ) is being_line ;

theorem :: AFF_4:25
for AS being ( ( V46() AffinSpace-like ) ( non empty V46() AffinSpace-like ) AffinSpace)
for a, b, c being ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) )
for X, Y being ( ( ) ( ) Subset of ) st X : ( ( ) ( ) Subset of ) is being_plane & Y : ( ( ) ( ) Subset of ) is being_plane & a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in X : ( ( ) ( ) Subset of ) & b : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in X : ( ( ) ( ) Subset of ) & c : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in X : ( ( ) ( ) Subset of ) & a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in Y : ( ( ) ( ) Subset of ) & b : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in Y : ( ( ) ( ) Subset of ) & c : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in Y : ( ( ) ( ) Subset of ) & not LIN a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) holds
X : ( ( ) ( ) Subset of ) = Y : ( ( ) ( ) Subset of ) ;

theorem :: AFF_4:26
for AS being ( ( V46() AffinSpace-like ) ( non empty V46() AffinSpace-like ) AffinSpace)
for X, Y, M, N being ( ( ) ( ) Subset of ) st X : ( ( ) ( ) Subset of ) is being_plane & Y : ( ( ) ( ) Subset of ) is being_plane & M : ( ( ) ( ) Subset of ) is being_line & N : ( ( ) ( ) Subset of ) is being_line & M : ( ( ) ( ) Subset of ) c= X : ( ( ) ( ) Subset of ) & N : ( ( ) ( ) Subset of ) c= X : ( ( ) ( ) Subset of ) & M : ( ( ) ( ) Subset of ) c= Y : ( ( ) ( ) Subset of ) & N : ( ( ) ( ) Subset of ) c= Y : ( ( ) ( ) Subset of ) & M : ( ( ) ( ) Subset of ) <> N : ( ( ) ( ) Subset of ) holds
X : ( ( ) ( ) Subset of ) = Y : ( ( ) ( ) Subset of ) ;

definition
let AS be ( ( V46() AffinSpace-like ) ( non empty V46() AffinSpace-like ) AffinSpace) ;
let a be ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ;
let K be ( ( ) ( ) Subset of ) ;
assume K : ( ( ) ( ) Subset of ) is being_line ;
func a * K -> ( ( ) ( ) Subset of ) means :: AFF_4:def 3
( a : ( ( ) ( ) Element of K24(K25(K25(AS : ( ( ) ( ) AffinStruct ) ,AS : ( ( ) ( ) AffinStruct ) ) : ( ( ) ( ) set ) ,K25(AS : ( ( ) ( ) AffinStruct ) ,AS : ( ( ) ( ) AffinStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) in it : ( ( ) ( ) Element of K24( the carrier of AS : ( ( ) ( ) AffinStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) & K : ( ( ) ( ) Element of AS : ( ( ) ( ) AffinStruct ) ) // it : ( ( ) ( ) Element of K24( the carrier of AS : ( ( ) ( ) AffinStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) );
end;

theorem :: AFF_4:27
for AS being ( ( V46() AffinSpace-like ) ( non empty V46() AffinSpace-like ) AffinSpace)
for a being ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) )
for A being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) is being_line holds
a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) * A : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset of ) is being_line ;

theorem :: AFF_4:28
for AS being ( ( V46() AffinSpace-like ) ( non empty V46() AffinSpace-like ) AffinSpace)
for a being ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) )
for X, M being ( ( ) ( ) Subset of ) st X : ( ( ) ( ) Subset of ) is being_plane & M : ( ( ) ( ) Subset of ) is being_line & a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in X : ( ( ) ( ) Subset of ) & M : ( ( ) ( ) Subset of ) c= X : ( ( ) ( ) Subset of ) holds
a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) * M : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset of ) c= X : ( ( ) ( ) Subset of ) ;

theorem :: AFF_4:29
for AS being ( ( V46() AffinSpace-like ) ( non empty V46() AffinSpace-like ) AffinSpace)
for a, b, c, d being ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) )
for X being ( ( ) ( ) Subset of ) st X : ( ( ) ( ) Subset of ) is being_plane & a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in X : ( ( ) ( ) Subset of ) & b : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in X : ( ( ) ( ) Subset of ) & c : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in X : ( ( ) ( ) Subset of ) & a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) <> b : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) holds
d : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in X : ( ( ) ( ) Subset of ) ;

theorem :: AFF_4:30
for AS being ( ( V46() AffinSpace-like ) ( non empty V46() AffinSpace-like ) AffinSpace)
for a being ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) )
for A being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) is being_line holds
( a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in A : ( ( ) ( ) Subset of ) iff a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) * A : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset of ) = A : ( ( ) ( ) Subset of ) ) ;

theorem :: AFF_4:31
for AS being ( ( V46() AffinSpace-like ) ( non empty V46() AffinSpace-like ) AffinSpace)
for a, q being ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) )
for A being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) is being_line holds
a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) * A : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset of ) = a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) * (q : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) * A : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset of ) ;

theorem :: AFF_4:32
for AS being ( ( V46() AffinSpace-like ) ( non empty V46() AffinSpace-like ) AffinSpace)
for a being ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) )
for K, M being ( ( ) ( ) Subset of ) st K : ( ( ) ( ) Subset of ) // M : ( ( ) ( ) Subset of ) holds
a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) * K : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset of ) = a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) * M : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset of ) ;

definition
let AS be ( ( V46() AffinSpace-like ) ( non empty V46() AffinSpace-like ) AffinSpace) ;
let X, Y be ( ( ) ( ) Subset of ) ;
pred X '||' Y means :: AFF_4:def 4
 for a being ( ( ) ( ) Element of ( ( ) ( ) set ) )
for A being ( ( ) ( ) Subset of ) st a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in Y : ( ( ) ( ) Element of AS : ( ( ) ( ) AffinStruct ) ) & A : ( ( ) ( ) Subset of ) is being_line & A : ( ( ) ( ) Subset of ) c= X : ( ( ) ( ) Element of K24(K25(K25(AS : ( ( ) ( ) AffinStruct ) ,AS : ( ( ) ( ) AffinStruct ) ) : ( ( ) ( ) set ) ,K25(AS : ( ( ) ( ) AffinStruct ) ,AS : ( ( ) ( ) AffinStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) holds
a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) * A : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset of ) c= Y : ( ( ) ( ) Element of AS : ( ( ) ( ) AffinStruct ) ) ;
end;

theorem :: AFF_4:33
for AS being ( ( V46() AffinSpace-like ) ( non empty V46() AffinSpace-like ) AffinSpace)
for X, Y being ( ( ) ( ) Subset of ) st X : ( ( ) ( ) Subset of ) c= Y : ( ( ) ( ) Subset of ) & ( ( X : ( ( ) ( ) Subset of ) is being_line & Y : ( ( ) ( ) Subset of ) is being_line ) or ( X : ( ( ) ( ) Subset of ) is being_plane & Y : ( ( ) ( ) Subset of ) is being_plane ) ) holds
X : ( ( ) ( ) Subset of ) = Y : ( ( ) ( ) Subset of ) ;

theorem :: AFF_4:34
for AS being ( ( V46() AffinSpace-like ) ( non empty V46() AffinSpace-like ) AffinSpace)
for X being ( ( ) ( ) Subset of ) st X : ( ( ) ( ) Subset of ) is being_plane holds
ex a, b, c being ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) st
( a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in X : ( ( ) ( ) Subset of ) & b : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in X : ( ( ) ( ) Subset of ) & c : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in X : ( ( ) ( ) Subset of ) & not LIN a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ) ;

theorem :: AFF_4:35
for AS being ( ( V46() AffinSpace-like ) ( non empty V46() AffinSpace-like ) AffinSpace)
for M, X being ( ( ) ( ) Subset of ) st M : ( ( ) ( ) Subset of ) is being_line & X : ( ( ) ( ) Subset of ) is being_plane holds
ex q being ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) st
( q : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in X : ( ( ) ( ) Subset of ) & not q : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in M : ( ( ) ( ) Subset of ) ) ;

theorem :: AFF_4:36
for AS being ( ( V46() AffinSpace-like ) ( non empty V46() AffinSpace-like ) AffinSpace)
for a being ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) )
for A being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) is being_line holds
ex X being ( ( ) ( ) Subset of ) st
( a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in X : ( ( ) ( ) Subset of ) & A : ( ( ) ( ) Subset of ) c= X : ( ( ) ( ) Subset of ) & X : ( ( ) ( ) Subset of ) is being_plane ) ;

theorem :: AFF_4:37
for AS being ( ( V46() AffinSpace-like ) ( non empty V46() AffinSpace-like ) AffinSpace)
for a, b, c being ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ex X being ( ( ) ( ) Subset of ) st
( a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in X : ( ( ) ( ) Subset of ) & b : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in X : ( ( ) ( ) Subset of ) & c : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in X : ( ( ) ( ) Subset of ) & X : ( ( ) ( ) Subset of ) is being_plane ) ;

theorem :: AFF_4:38
for AS being ( ( V46() AffinSpace-like ) ( non empty V46() AffinSpace-like ) AffinSpace)
for q being ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) )
for M, N being ( ( ) ( ) Subset of ) st q : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in M : ( ( ) ( ) Subset of ) & q : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in N : ( ( ) ( ) Subset of ) & M : ( ( ) ( ) Subset of ) is being_line & N : ( ( ) ( ) Subset of ) is being_line holds
ex X being ( ( ) ( ) Subset of ) st
( M : ( ( ) ( ) Subset of ) c= X : ( ( ) ( ) Subset of ) & N : ( ( ) ( ) Subset of ) c= X : ( ( ) ( ) Subset of ) & X : ( ( ) ( ) Subset of ) is being_plane ) ;

theorem :: AFF_4:39
for AS being ( ( V46() AffinSpace-like ) ( non empty V46() AffinSpace-like ) AffinSpace)
for M, N being ( ( ) ( ) Subset of ) st M : ( ( ) ( ) Subset of ) // N : ( ( ) ( ) Subset of ) holds
ex X being ( ( ) ( ) Subset of ) st
( M : ( ( ) ( ) Subset of ) c= X : ( ( ) ( ) Subset of ) & N : ( ( ) ( ) Subset of ) c= X : ( ( ) ( ) Subset of ) & X : ( ( ) ( ) Subset of ) is being_plane ) ;

theorem :: AFF_4:40
for AS being ( ( V46() AffinSpace-like ) ( non empty V46() AffinSpace-like ) AffinSpace)
for M, N being ( ( ) ( ) Subset of ) st M : ( ( ) ( ) Subset of ) is being_line & N : ( ( ) ( ) Subset of ) is being_line holds
( M : ( ( ) ( ) Subset of ) // N : ( ( ) ( ) Subset of ) iff M : ( ( ) ( ) Subset of ) '||' N : ( ( ) ( ) Subset of ) ) ;

theorem :: AFF_4:41
for AS being ( ( V46() AffinSpace-like ) ( non empty V46() AffinSpace-like ) AffinSpace)
for M, X being ( ( ) ( ) Subset of ) st M : ( ( ) ( ) Subset of ) is being_line & X : ( ( ) ( ) Subset of ) is being_plane holds
( M : ( ( ) ( ) Subset of ) '||' X : ( ( ) ( ) Subset of ) iff ex N being ( ( ) ( ) Subset of ) st
( N : ( ( ) ( ) Subset of ) c= X : ( ( ) ( ) Subset of ) & ( M : ( ( ) ( ) Subset of ) // N : ( ( ) ( ) Subset of ) or N : ( ( ) ( ) Subset of ) // M : ( ( ) ( ) Subset of ) ) ) ) ;

theorem :: AFF_4:42
for AS being ( ( V46() AffinSpace-like ) ( non empty V46() AffinSpace-like ) AffinSpace)
for M, X being ( ( ) ( ) Subset of ) st M : ( ( ) ( ) Subset of ) is being_line & X : ( ( ) ( ) Subset of ) is being_plane & M : ( ( ) ( ) Subset of ) c= X : ( ( ) ( ) Subset of ) holds
M : ( ( ) ( ) Subset of ) '||' X : ( ( ) ( ) Subset of ) ;

theorem :: AFF_4:43
for AS being ( ( V46() AffinSpace-like ) ( non empty V46() AffinSpace-like ) AffinSpace)
for a being ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) )
for A, X being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) is being_line & X : ( ( ) ( ) Subset of ) is being_plane & a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in A : ( ( ) ( ) Subset of ) & a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in X : ( ( ) ( ) Subset of ) & A : ( ( ) ( ) Subset of ) '||' X : ( ( ) ( ) Subset of ) holds
A : ( ( ) ( ) Subset of ) c= X : ( ( ) ( ) Subset of ) ;

definition
let AS be ( ( V46() AffinSpace-like ) ( non empty V46() AffinSpace-like ) AffinSpace) ;
let K, M, N be ( ( ) ( ) Subset of ) ;
pred K,M,N is_coplanar means :: AFF_4:def 5
 ex X being ( ( ) ( ) Subset of ) st
( K : ( ( ) ( ) Element of K24(K25(K25(AS : ( ( ) ( ) AffinStruct ) ,AS : ( ( ) ( ) AffinStruct ) ) : ( ( ) ( ) set ) ,K25(AS : ( ( ) ( ) AffinStruct ) ,AS : ( ( ) ( ) AffinStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) c= X : ( ( ) ( ) Subset of ) & M : ( ( ) ( ) Element of AS : ( ( ) ( ) AffinStruct ) ) c= X : ( ( ) ( ) Subset of ) & N : ( ( ) ( ) Element of K24( the carrier of AS : ( ( ) ( ) AffinStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) c= X : ( ( ) ( ) Subset of ) & X : ( ( ) ( ) Subset of ) is being_plane );
end;

theorem :: AFF_4:44
for AS being ( ( V46() AffinSpace-like ) ( non empty V46() AffinSpace-like ) AffinSpace)
for K, M, N being ( ( ) ( ) Subset of ) st K : ( ( ) ( ) Subset of ) ,M : ( ( ) ( ) Subset of ) ,N : ( ( ) ( ) Subset of ) is_coplanar holds
( K : ( ( ) ( ) Subset of ) ,N : ( ( ) ( ) Subset of ) ,M : ( ( ) ( ) Subset of ) is_coplanar & M : ( ( ) ( ) Subset of ) ,K : ( ( ) ( ) Subset of ) ,N : ( ( ) ( ) Subset of ) is_coplanar & M : ( ( ) ( ) Subset of ) ,N : ( ( ) ( ) Subset of ) ,K : ( ( ) ( ) Subset of ) is_coplanar & N : ( ( ) ( ) Subset of ) ,K : ( ( ) ( ) Subset of ) ,M : ( ( ) ( ) Subset of ) is_coplanar & N : ( ( ) ( ) Subset of ) ,M : ( ( ) ( ) Subset of ) ,K : ( ( ) ( ) Subset of ) is_coplanar ) ;

theorem :: AFF_4:45
for AS being ( ( V46() AffinSpace-like ) ( non empty V46() AffinSpace-like ) AffinSpace)
for M, N, K, A being ( ( ) ( ) Subset of ) st M : ( ( ) ( ) Subset of ) is being_line & N : ( ( ) ( ) Subset of ) is being_line & M : ( ( ) ( ) Subset of ) ,N : ( ( ) ( ) Subset of ) ,K : ( ( ) ( ) Subset of ) is_coplanar & M : ( ( ) ( ) Subset of ) ,N : ( ( ) ( ) Subset of ) ,A : ( ( ) ( ) Subset of ) is_coplanar & M : ( ( ) ( ) Subset of ) <> N : ( ( ) ( ) Subset of ) holds
M : ( ( ) ( ) Subset of ) ,K : ( ( ) ( ) Subset of ) ,A : ( ( ) ( ) Subset of ) is_coplanar ;

theorem :: AFF_4:46
for AS being ( ( V46() AffinSpace-like ) ( non empty V46() AffinSpace-like ) AffinSpace)
for K, M, X, A being ( ( ) ( ) Subset of ) st K : ( ( ) ( ) Subset of ) is being_line & M : ( ( ) ( ) Subset of ) is being_line & X : ( ( ) ( ) Subset of ) is being_plane & K : ( ( ) ( ) Subset of ) c= X : ( ( ) ( ) Subset of ) & M : ( ( ) ( ) Subset of ) c= X : ( ( ) ( ) Subset of ) & K : ( ( ) ( ) Subset of ) <> M : ( ( ) ( ) Subset of ) holds
( K : ( ( ) ( ) Subset of ) ,M : ( ( ) ( ) Subset of ) ,A : ( ( ) ( ) Subset of ) is_coplanar iff A : ( ( ) ( ) Subset of ) c= X : ( ( ) ( ) Subset of ) ) ;

theorem :: AFF_4:47
for AS being ( ( V46() AffinSpace-like ) ( non empty V46() AffinSpace-like ) AffinSpace)
for q being ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) )
for K, M being ( ( ) ( ) Subset of ) st q : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in K : ( ( ) ( ) Subset of ) & q : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in M : ( ( ) ( ) Subset of ) & K : ( ( ) ( ) Subset of ) is being_line & M : ( ( ) ( ) Subset of ) is being_line holds
( K : ( ( ) ( ) Subset of ) ,M : ( ( ) ( ) Subset of ) ,M : ( ( ) ( ) Subset of ) is_coplanar & M : ( ( ) ( ) Subset of ) ,K : ( ( ) ( ) Subset of ) ,M : ( ( ) ( ) Subset of ) is_coplanar & M : ( ( ) ( ) Subset of ) ,M : ( ( ) ( ) Subset of ) ,K : ( ( ) ( ) Subset of ) is_coplanar ) ;

theorem :: AFF_4:48
for AS being ( ( V46() AffinSpace-like ) ( non empty V46() AffinSpace-like ) AffinSpace)
for X being ( ( ) ( ) Subset of ) st AS : ( ( V46() AffinSpace-like ) ( non empty V46() AffinSpace-like ) AffinSpace) is not ( ( V46() AffinSpace-like 2-dimensional ) ( non empty V46() AffinSpace-like 2-dimensional ) AffinPlane) & X : ( ( ) ( ) Subset of ) is being_plane holds
ex q being ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) st not q : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in X : ( ( ) ( ) Subset of ) ;

theorem :: AFF_4:49
for AS being ( ( V46() AffinSpace-like ) ( non empty V46() AffinSpace-like ) AffinSpace)
for q, a, b, c, a9, b9, c9 being ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) )
for A, P, C being ( ( ) ( ) Subset of ) st AS : ( ( V46() AffinSpace-like ) ( non empty V46() AffinSpace-like ) AffinSpace) is not ( ( V46() AffinSpace-like 2-dimensional ) ( non empty V46() AffinSpace-like 2-dimensional ) AffinPlane) & q : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in A : ( ( ) ( ) Subset of ) & q : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in P : ( ( ) ( ) Subset of ) & q : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in C : ( ( ) ( ) Subset of ) & q : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) <> a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) & q : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) <> b : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) & q : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) <> c : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in A : ( ( ) ( ) Subset of ) & a9 : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in A : ( ( ) ( ) Subset of ) & b : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in P : ( ( ) ( ) Subset of ) & b9 : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in P : ( ( ) ( ) Subset of ) & c : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in C : ( ( ) ( ) Subset of ) & c9 : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in C : ( ( ) ( ) Subset of ) & A : ( ( ) ( ) Subset of ) is being_line & P : ( ( ) ( ) Subset of ) is being_line & C : ( ( ) ( ) Subset of ) is being_line & A : ( ( ) ( ) Subset of ) <> P : ( ( ) ( ) Subset of ) & A : ( ( ) ( ) Subset of ) <> C : ( ( ) ( ) Subset of ) & a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) // a9 : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) // a9 : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) holds
b : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) // b9 : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ;

theorem :: AFF_4:50
for AS being ( ( V46() AffinSpace-like ) ( non empty V46() AffinSpace-like ) AffinSpace) st AS : ( ( V46() AffinSpace-like ) ( non empty V46() AffinSpace-like ) AffinSpace) is not ( ( V46() AffinSpace-like 2-dimensional ) ( non empty V46() AffinSpace-like 2-dimensional ) AffinPlane) holds
AS : ( ( V46() AffinSpace-like ) ( non empty V46() AffinSpace-like ) AffinSpace) is Desarguesian ;

theorem :: AFF_4:51
for AS being ( ( V46() AffinSpace-like ) ( non empty V46() AffinSpace-like ) AffinSpace)
for a, a9, b, b9, c, c9 being ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) )
for A, P, C being ( ( ) ( ) Subset of ) st AS : ( ( V46() AffinSpace-like ) ( non empty V46() AffinSpace-like ) AffinSpace) is not ( ( V46() AffinSpace-like 2-dimensional ) ( non empty V46() AffinSpace-like 2-dimensional ) AffinPlane) & A : ( ( ) ( ) Subset of ) // P : ( ( ) ( ) Subset of ) & A : ( ( ) ( ) Subset of ) // C : ( ( ) ( ) Subset of ) & a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in A : ( ( ) ( ) Subset of ) & a9 : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in A : ( ( ) ( ) Subset of ) & b : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in P : ( ( ) ( ) Subset of ) & b9 : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in P : ( ( ) ( ) Subset of ) & c : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in C : ( ( ) ( ) Subset of ) & c9 : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in C : ( ( ) ( ) Subset of ) & A : ( ( ) ( ) Subset of ) is being_line & P : ( ( ) ( ) Subset of ) is being_line & C : ( ( ) ( ) Subset of ) is being_line & A : ( ( ) ( ) Subset of ) <> P : ( ( ) ( ) Subset of ) & A : ( ( ) ( ) Subset of ) <> C : ( ( ) ( ) Subset of ) & a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) // a9 : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) // a9 : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) holds
b : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) // b9 : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ;

theorem :: AFF_4:52
for AS being ( ( V46() AffinSpace-like ) ( non empty V46() AffinSpace-like ) AffinSpace) st AS : ( ( V46() AffinSpace-like ) ( non empty V46() AffinSpace-like ) AffinSpace) is not ( ( V46() AffinSpace-like 2-dimensional ) ( non empty V46() AffinSpace-like 2-dimensional ) AffinPlane) holds
AS : ( ( V46() AffinSpace-like ) ( non empty V46() AffinSpace-like ) AffinSpace) is translational ;

theorem :: AFF_4:53
for AS being ( ( V46() AffinSpace-like ) ( non empty V46() AffinSpace-like ) AffinSpace)
for a, b, c, a9, b9 being ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) st AS : ( ( V46() AffinSpace-like ) ( non empty V46() AffinSpace-like ) AffinSpace) is ( ( V46() AffinSpace-like 2-dimensional ) ( non empty V46() AffinSpace-like 2-dimensional ) AffinPlane) & not LIN a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) holds
ex c9 being ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) st
( a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) // a9 : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) & b : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) // b9 : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ) ;

theorem :: AFF_4:54
for AS being ( ( V46() AffinSpace-like ) ( non empty V46() AffinSpace-like ) AffinSpace)
for a, b, c, a9, b9 being ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) st not LIN a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) & a9 : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) <> b9 : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) // a9 : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) holds
ex c9 being ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) st
( a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) // a9 : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) & b : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) // b9 : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ) ;

theorem :: AFF_4:55
for AS being ( ( V46() AffinSpace-like ) ( non empty V46() AffinSpace-like ) AffinSpace)
for X, Y being ( ( ) ( ) Subset of ) st X : ( ( ) ( ) Subset of ) is being_plane & Y : ( ( ) ( ) Subset of ) is being_plane holds
( X : ( ( ) ( ) Subset of ) '||' Y : ( ( ) ( ) Subset of ) iff ex A, P, M, N being ( ( ) ( ) Subset of ) st
( not A : ( ( ) ( ) Subset of ) // P : ( ( ) ( ) Subset of ) & A : ( ( ) ( ) Subset of ) c= X : ( ( ) ( ) Subset of ) & P : ( ( ) ( ) Subset of ) c= X : ( ( ) ( ) Subset of ) & M : ( ( ) ( ) Subset of ) c= Y : ( ( ) ( ) Subset of ) & N : ( ( ) ( ) Subset of ) c= Y : ( ( ) ( ) Subset of ) & ( A : ( ( ) ( ) Subset of ) // M : ( ( ) ( ) Subset of ) or M : ( ( ) ( ) Subset of ) // A : ( ( ) ( ) Subset of ) ) & ( P : ( ( ) ( ) Subset of ) // N : ( ( ) ( ) Subset of ) or N : ( ( ) ( ) Subset of ) // P : ( ( ) ( ) Subset of ) ) ) ) ;

theorem :: AFF_4:56
for AS being ( ( V46() AffinSpace-like ) ( non empty V46() AffinSpace-like ) AffinSpace)
for A, M, X being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) // M : ( ( ) ( ) Subset of ) & M : ( ( ) ( ) Subset of ) '||' X : ( ( ) ( ) Subset of ) holds
A : ( ( ) ( ) Subset of ) '||' X : ( ( ) ( ) Subset of ) ;

theorem :: AFF_4:57
for AS being ( ( V46() AffinSpace-like ) ( non empty V46() AffinSpace-like ) AffinSpace)
for X being ( ( ) ( ) Subset of ) st X : ( ( ) ( ) Subset of ) is being_plane holds
X : ( ( ) ( ) Subset of ) '||' X : ( ( ) ( ) Subset of ) ;

theorem :: AFF_4:58
for AS being ( ( V46() AffinSpace-like ) ( non empty V46() AffinSpace-like ) AffinSpace)
for X, Y being ( ( ) ( ) Subset of ) st X : ( ( ) ( ) Subset of ) is being_plane & Y : ( ( ) ( ) Subset of ) is being_plane & X : ( ( ) ( ) Subset of ) '||' Y : ( ( ) ( ) Subset of ) holds
Y : ( ( ) ( ) Subset of ) '||' X : ( ( ) ( ) Subset of ) ;

theorem :: AFF_4:59
for AS being ( ( V46() AffinSpace-like ) ( non empty V46() AffinSpace-like ) AffinSpace)
for X being ( ( ) ( ) Subset of ) st X : ( ( ) ( ) Subset of ) is being_plane holds
X : ( ( ) ( ) Subset of ) <> {} : ( ( ) ( empty ) set ) ;

theorem :: AFF_4:60
for AS being ( ( V46() AffinSpace-like ) ( non empty V46() AffinSpace-like ) AffinSpace)
for X, Y, Z being ( ( ) ( ) Subset of ) st X : ( ( ) ( ) Subset of ) '||' Y : ( ( ) ( ) Subset of ) & Y : ( ( ) ( ) Subset of ) '||' Z : ( ( ) ( ) Subset of ) & Y : ( ( ) ( ) Subset of ) <> {} : ( ( ) ( empty ) set ) holds
X : ( ( ) ( ) Subset of ) '||' Z : ( ( ) ( ) Subset of ) ;

theorem :: AFF_4:61
for AS being ( ( V46() AffinSpace-like ) ( non empty V46() AffinSpace-like ) AffinSpace)
for X, Y, Z being ( ( ) ( ) Subset of ) st X : ( ( ) ( ) Subset of ) is being_plane & Y : ( ( ) ( ) Subset of ) is being_plane & Z : ( ( ) ( ) Subset of ) is being_plane & ( ( X : ( ( ) ( ) Subset of ) '||' Y : ( ( ) ( ) Subset of ) & Y : ( ( ) ( ) Subset of ) '||' Z : ( ( ) ( ) Subset of ) ) or ( X : ( ( ) ( ) Subset of ) '||' Y : ( ( ) ( ) Subset of ) & Z : ( ( ) ( ) Subset of ) '||' Y : ( ( ) ( ) Subset of ) ) or ( Y : ( ( ) ( ) Subset of ) '||' X : ( ( ) ( ) Subset of ) & Y : ( ( ) ( ) Subset of ) '||' Z : ( ( ) ( ) Subset of ) ) or ( Y : ( ( ) ( ) Subset of ) '||' X : ( ( ) ( ) Subset of ) & Z : ( ( ) ( ) Subset of ) '||' Y : ( ( ) ( ) Subset of ) ) ) holds
X : ( ( ) ( ) Subset of ) '||' Z : ( ( ) ( ) Subset of ) ;

theorem :: AFF_4:62
for AS being ( ( V46() AffinSpace-like ) ( non empty V46() AffinSpace-like ) AffinSpace)
for a being ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) )
for X, Y being ( ( ) ( ) Subset of ) st X : ( ( ) ( ) Subset of ) is being_plane & Y : ( ( ) ( ) Subset of ) is being_plane & a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in X : ( ( ) ( ) Subset of ) & a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in Y : ( ( ) ( ) Subset of ) & X : ( ( ) ( ) Subset of ) '||' Y : ( ( ) ( ) Subset of ) holds
X : ( ( ) ( ) Subset of ) = Y : ( ( ) ( ) Subset of ) ;

theorem :: AFF_4:63
for AS being ( ( V46() AffinSpace-like ) ( non empty V46() AffinSpace-like ) AffinSpace)
for a, b, c, d being ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) )
for X, Y, Z being ( ( ) ( ) Subset of ) st X : ( ( ) ( ) Subset of ) is being_plane & Y : ( ( ) ( ) Subset of ) is being_plane & Z : ( ( ) ( ) Subset of ) is being_plane & X : ( ( ) ( ) Subset of ) '||' Y : ( ( ) ( ) Subset of ) & X : ( ( ) ( ) Subset of ) <> Y : ( ( ) ( ) Subset of ) & a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in X : ( ( ) ( ) Subset of ) /\ Z : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K24( the carrier of b1 : ( ( V46() AffinSpace-like ) ( non empty V46() AffinSpace-like ) AffinSpace) : ( ( ) ( non empty V5() ) set ) ) : ( ( ) ( ) set ) ) & b : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in X : ( ( ) ( ) Subset of ) /\ Z : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K24( the carrier of b1 : ( ( V46() AffinSpace-like ) ( non empty V46() AffinSpace-like ) AffinSpace) : ( ( ) ( non empty V5() ) set ) ) : ( ( ) ( ) set ) ) & c : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in Y : ( ( ) ( ) Subset of ) /\ Z : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K24( the carrier of b1 : ( ( V46() AffinSpace-like ) ( non empty V46() AffinSpace-like ) AffinSpace) : ( ( ) ( non empty V5() ) set ) ) : ( ( ) ( ) set ) ) & d : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in Y : ( ( ) ( ) Subset of ) /\ Z : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K24( the carrier of b1 : ( ( V46() AffinSpace-like ) ( non empty V46() AffinSpace-like ) AffinSpace) : ( ( ) ( non empty V5() ) set ) ) : ( ( ) ( ) set ) ) holds
a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ;

theorem :: AFF_4:64
for AS being ( ( V46() AffinSpace-like ) ( non empty V46() AffinSpace-like ) AffinSpace)
for a, b, c, d being ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) )
for X, Y, Z being ( ( ) ( ) Subset of ) st X : ( ( ) ( ) Subset of ) is being_plane & Y : ( ( ) ( ) Subset of ) is being_plane & Z : ( ( ) ( ) Subset of ) is being_plane & X : ( ( ) ( ) Subset of ) '||' Y : ( ( ) ( ) Subset of ) & a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in X : ( ( ) ( ) Subset of ) /\ Z : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K24( the carrier of b1 : ( ( V46() AffinSpace-like ) ( non empty V46() AffinSpace-like ) AffinSpace) : ( ( ) ( non empty V5() ) set ) ) : ( ( ) ( ) set ) ) & b : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in X : ( ( ) ( ) Subset of ) /\ Z : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K24( the carrier of b1 : ( ( V46() AffinSpace-like ) ( non empty V46() AffinSpace-like ) AffinSpace) : ( ( ) ( non empty V5() ) set ) ) : ( ( ) ( ) set ) ) & c : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in Y : ( ( ) ( ) Subset of ) /\ Z : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K24( the carrier of b1 : ( ( V46() AffinSpace-like ) ( non empty V46() AffinSpace-like ) AffinSpace) : ( ( ) ( non empty V5() ) set ) ) : ( ( ) ( ) set ) ) & d : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in Y : ( ( ) ( ) Subset of ) /\ Z : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K24( the carrier of b1 : ( ( V46() AffinSpace-like ) ( non empty V46() AffinSpace-like ) AffinSpace) : ( ( ) ( non empty V5() ) set ) ) : ( ( ) ( ) set ) ) & X : ( ( ) ( ) Subset of ) <> Y : ( ( ) ( ) Subset of ) & a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) <> b : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) & c : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) <> d : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) holds
X : ( ( ) ( ) Subset of ) /\ Z : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K24( the carrier of b1 : ( ( V46() AffinSpace-like ) ( non empty V46() AffinSpace-like ) AffinSpace) : ( ( ) ( non empty V5() ) set ) ) : ( ( ) ( ) set ) ) // Y : ( ( ) ( ) Subset of ) /\ Z : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K24( the carrier of b1 : ( ( V46() AffinSpace-like ) ( non empty V46() AffinSpace-like ) AffinSpace) : ( ( ) ( non empty V5() ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: AFF_4:65
for AS being ( ( V46() AffinSpace-like ) ( non empty V46() AffinSpace-like ) AffinSpace)
for a being ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) )
for X being ( ( ) ( ) Subset of ) st X : ( ( ) ( ) Subset of ) is being_plane holds
ex Y being ( ( ) ( ) Subset of ) st
( a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in Y : ( ( ) ( ) Subset of ) & X : ( ( ) ( ) Subset of ) '||' Y : ( ( ) ( ) Subset of ) & Y : ( ( ) ( ) Subset of ) is being_plane ) ;

definition
let AS be ( ( V46() AffinSpace-like ) ( non empty V46() AffinSpace-like ) AffinSpace) ;
let a be ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) ;
let X be ( ( ) ( ) Subset of ) ;
assume X : ( ( ) ( ) Subset of ) is being_plane ;
func a + X -> ( ( ) ( ) Subset of ) means :: AFF_4:def 6
( a : ( ( ) ( ) Element of K24(K25(K25(AS : ( ( ) ( ) AffinStruct ) ,AS : ( ( ) ( ) AffinStruct ) ) : ( ( ) ( ) set ) ,K25(AS : ( ( ) ( ) AffinStruct ) ,AS : ( ( ) ( ) AffinStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) in it : ( ( ) ( ) Element of K24( the carrier of AS : ( ( ) ( ) AffinStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) & X : ( ( ) ( ) Element of AS : ( ( ) ( ) AffinStruct ) ) '||' it : ( ( ) ( ) Element of K24( the carrier of AS : ( ( ) ( ) AffinStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) & it : ( ( ) ( ) Element of K24( the carrier of AS : ( ( ) ( ) AffinStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) is being_plane );
end;

theorem :: AFF_4:66
for AS being ( ( V46() AffinSpace-like ) ( non empty V46() AffinSpace-like ) AffinSpace)
for a being ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) )
for X being ( ( ) ( ) Subset of ) st X : ( ( ) ( ) Subset of ) is being_plane holds
( a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) in X : ( ( ) ( ) Subset of ) iff a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) + X : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset of ) = X : ( ( ) ( ) Subset of ) ) ;

theorem :: AFF_4:67
for AS being ( ( V46() AffinSpace-like ) ( non empty V46() AffinSpace-like ) AffinSpace)
for a, q being ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) )
for X being ( ( ) ( ) Subset of ) st X : ( ( ) ( ) Subset of ) is being_plane holds
a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) + X : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset of ) = a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) + (q : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) + X : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset of ) ;

theorem :: AFF_4:68
for AS being ( ( V46() AffinSpace-like ) ( non empty V46() AffinSpace-like ) AffinSpace)
for a being ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) )
for A, X being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) is being_line & X : ( ( ) ( ) Subset of ) is being_plane & A : ( ( ) ( ) Subset of ) '||' X : ( ( ) ( ) Subset of ) holds
a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) * A : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset of ) c= a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) + X : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset of ) ;

theorem :: AFF_4:69
for AS being ( ( V46() AffinSpace-like ) ( non empty V46() AffinSpace-like ) AffinSpace)
for a being ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) )
for X, Y being ( ( ) ( ) Subset of ) st X : ( ( ) ( ) Subset of ) is being_plane & Y : ( ( ) ( ) Subset of ) is being_plane & X : ( ( ) ( ) Subset of ) '||' Y : ( ( ) ( ) Subset of ) holds
a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) + X : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset of ) = a : ( ( ) ( ) Element of ( ( ) ( non empty V5() ) set ) ) + Y : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset of ) ;