:: AFF_3 semantic presentation

begin

definition
let AP be ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) ;
attr AP is satisfying_DES1 means :: AFF_3:def 1
 for A, P, C being ( ( ) ( ) Subset of )
for o, a, a9, b, b9, c, c9, p, q being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st A : ( ( ) ( ) Subset of ) is being_line & P : ( ( ) ( ) Subset of ) is being_line & C : ( ( ) ( ) Subset of ) is being_line & P : ( ( ) ( ) Subset of ) <> A : ( ( ) ( ) Subset of ) & P : ( ( ) ( ) Subset of ) <> C : ( ( ) ( ) Subset of ) & A : ( ( ) ( ) Subset of ) <> C : ( ( ) ( ) Subset of ) & o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in A : ( ( ) ( ) Subset of ) & a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in A : ( ( ) ( ) Subset of ) & a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in A : ( ( ) ( ) Subset of ) & o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in P : ( ( ) ( ) Subset of ) & b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in P : ( ( ) ( ) Subset of ) & b9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in P : ( ( ) ( ) Subset of ) & o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in C : ( ( ) ( ) Subset of ) & c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in C : ( ( ) ( ) Subset of ) & c9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in C : ( ( ) ( ) Subset of ) & o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) <> a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) <> b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) <> c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) <> q : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & not LIN b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & not LIN b9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) <> a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & LIN b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & LIN b9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & LIN b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & LIN b9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) holds
a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ;
end;

definition
let AP be ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) ;
attr AP is satisfying_DES1_1 means :: AFF_3:def 2
 for A, P, C being ( ( ) ( ) Subset of )
for o, a, a9, b, b9, c, c9, p, q being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st A : ( ( ) ( ) Subset of ) is being_line & P : ( ( ) ( ) Subset of ) is being_line & C : ( ( ) ( ) Subset of ) is being_line & P : ( ( ) ( ) Subset of ) <> A : ( ( ) ( ) Subset of ) & P : ( ( ) ( ) Subset of ) <> C : ( ( ) ( ) Subset of ) & A : ( ( ) ( ) Subset of ) <> C : ( ( ) ( ) Subset of ) & o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in A : ( ( ) ( ) Subset of ) & a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in A : ( ( ) ( ) Subset of ) & a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in A : ( ( ) ( ) Subset of ) & o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in P : ( ( ) ( ) Subset of ) & b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in P : ( ( ) ( ) Subset of ) & b9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in P : ( ( ) ( ) Subset of ) & o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in C : ( ( ) ( ) Subset of ) & c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in C : ( ( ) ( ) Subset of ) & c9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in C : ( ( ) ( ) Subset of ) & o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) <> a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) <> b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) <> c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) <> q : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) <> q : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & not LIN b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & not LIN b9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & LIN b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & LIN b9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & LIN b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & LIN b9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) holds
a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ;
end;

definition
let AP be ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) ;
attr AP is satisfying_DES1_2 means :: AFF_3:def 3
 for A, P, C being ( ( ) ( ) Subset of )
for o, a, a9, b, b9, c, c9, p, q being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st A : ( ( ) ( ) Subset of ) is being_line & P : ( ( ) ( ) Subset of ) is being_line & C : ( ( ) ( ) Subset of ) is being_line & P : ( ( ) ( ) Subset of ) <> A : ( ( ) ( ) Subset of ) & P : ( ( ) ( ) Subset of ) <> C : ( ( ) ( ) Subset of ) & A : ( ( ) ( ) Subset of ) <> C : ( ( ) ( ) Subset of ) & o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in A : ( ( ) ( ) Subset of ) & a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in A : ( ( ) ( ) Subset of ) & a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in A : ( ( ) ( ) Subset of ) & o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in P : ( ( ) ( ) Subset of ) & b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in P : ( ( ) ( ) Subset of ) & b9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in P : ( ( ) ( ) Subset of ) & c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in C : ( ( ) ( ) Subset of ) & c9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in C : ( ( ) ( ) Subset of ) & o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) <> a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) <> b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) <> c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) <> q : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & not LIN b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & not LIN b9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) <> c9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & LIN b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & LIN b9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & LIN b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & LIN b9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) holds
o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in C : ( ( ) ( ) Subset of ) ;
end;

definition
let AP be ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) ;
attr AP is satisfying_DES1_3 means :: AFF_3:def 4
 for A, P, C being ( ( ) ( ) Subset of )
for o, a, a9, b, b9, c, c9, p, q being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st A : ( ( ) ( ) Subset of ) is being_line & P : ( ( ) ( ) Subset of ) is being_line & C : ( ( ) ( ) Subset of ) is being_line & P : ( ( ) ( ) Subset of ) <> A : ( ( ) ( ) Subset of ) & P : ( ( ) ( ) Subset of ) <> C : ( ( ) ( ) Subset of ) & A : ( ( ) ( ) Subset of ) <> C : ( ( ) ( ) Subset of ) & o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in A : ( ( ) ( ) Subset of ) & a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in A : ( ( ) ( ) Subset of ) & a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in A : ( ( ) ( ) Subset of ) & b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in P : ( ( ) ( ) Subset of ) & b9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in P : ( ( ) ( ) Subset of ) & o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in C : ( ( ) ( ) Subset of ) & c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in C : ( ( ) ( ) Subset of ) & c9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in C : ( ( ) ( ) Subset of ) & o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) <> a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) <> b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) <> c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) <> q : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & not LIN b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & not LIN b9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) <> b9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) <> a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & LIN b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & LIN b9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & LIN b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & LIN b9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) holds
o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in P : ( ( ) ( ) Subset of ) ;
end;

definition
let AP be ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) ;
attr AP is satisfying_DES2 means :: AFF_3:def 5
 for A, P, C being ( ( ) ( ) Subset of )
for a, a9, b, b9, c, c9, p, q being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st 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 ) & P : ( ( ) ( ) Subset of ) <> C : ( ( ) ( ) Subset of ) & a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in A : ( ( ) ( ) Subset of ) & a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in A : ( ( ) ( ) Subset of ) & b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in P : ( ( ) ( ) Subset of ) & b9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in P : ( ( ) ( ) Subset of ) & c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in C : ( ( ) ( ) Subset of ) & c9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in C : ( ( ) ( ) Subset of ) & A : ( ( ) ( ) Subset of ) // P : ( ( ) ( ) Subset of ) & A : ( ( ) ( ) Subset of ) // C : ( ( ) ( ) Subset of ) & not LIN b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & not LIN b9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) <> q : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) <> a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & LIN b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & LIN b9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & LIN b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & LIN b9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) holds
a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ;
end;

definition
let AP be ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) ;
attr AP is satisfying_DES2_1 means :: AFF_3:def 6
 for A, P, C being ( ( ) ( ) Subset of )
for a, a9, b, b9, c, c9, p, q being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st 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 ) & P : ( ( ) ( ) Subset of ) <> C : ( ( ) ( ) Subset of ) & a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in A : ( ( ) ( ) Subset of ) & a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in A : ( ( ) ( ) Subset of ) & b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in P : ( ( ) ( ) Subset of ) & b9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in P : ( ( ) ( ) Subset of ) & c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in C : ( ( ) ( ) Subset of ) & c9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in C : ( ( ) ( ) Subset of ) & A : ( ( ) ( ) Subset of ) // P : ( ( ) ( ) Subset of ) & A : ( ( ) ( ) Subset of ) // C : ( ( ) ( ) Subset of ) & not LIN b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & not LIN b9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) <> q : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & LIN b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & LIN b9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & LIN b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & LIN b9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) holds
a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ;
end;

definition
let AP be ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) ;
attr AP is satisfying_DES2_2 means :: AFF_3:def 7
 for A, P, C being ( ( ) ( ) Subset of )
for a, a9, b, b9, c, c9, p, q being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st 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 ) & P : ( ( ) ( ) Subset of ) <> C : ( ( ) ( ) Subset of ) & a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in A : ( ( ) ( ) Subset of ) & a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in A : ( ( ) ( ) Subset of ) & b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in P : ( ( ) ( ) Subset of ) & b9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in P : ( ( ) ( ) Subset of ) & c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in C : ( ( ) ( ) Subset of ) & c9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in C : ( ( ) ( ) Subset of ) & A : ( ( ) ( ) Subset of ) // C : ( ( ) ( ) Subset of ) & not LIN b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & not LIN b9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) <> q : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) <> a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & LIN b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & LIN b9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & LIN b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & LIN b9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) holds
A : ( ( ) ( ) Subset of ) // P : ( ( ) ( ) Subset of ) ;
end;

definition
let AP be ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) ;
attr AP is satisfying_DES2_3 means :: AFF_3:def 8
 for A, P, C being ( ( ) ( ) Subset of )
for a, a9, b, b9, c, c9, p, q being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st 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 ) & P : ( ( ) ( ) Subset of ) <> C : ( ( ) ( ) Subset of ) & a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in A : ( ( ) ( ) Subset of ) & a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in A : ( ( ) ( ) Subset of ) & b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in P : ( ( ) ( ) Subset of ) & b9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in P : ( ( ) ( ) Subset of ) & c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in C : ( ( ) ( ) Subset of ) & c9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in C : ( ( ) ( ) Subset of ) & A : ( ( ) ( ) Subset of ) // P : ( ( ) ( ) Subset of ) & not LIN b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & not LIN b9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) <> q : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) <> c9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & LIN b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & LIN b9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & LIN b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & LIN b9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) holds
A : ( ( ) ( ) Subset of ) // C : ( ( ) ( ) Subset of ) ;
end;

theorem :: AFF_3:1
for AP being ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) st AP : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) is satisfying_DES1 holds
AP : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) is satisfying_DES1_1 ;

theorem :: AFF_3:2
for AP being ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) st AP : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) is satisfying_DES1_1 holds
AP : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) is satisfying_DES1 ;

theorem :: AFF_3:3
for AP being ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) st AP : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) is Desarguesian holds
AP : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) is satisfying_DES1 ;

theorem :: AFF_3:4
for AP being ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) st AP : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) is Desarguesian holds
AP : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) is satisfying_DES1_2 ;

theorem :: AFF_3:5
for AP being ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) st AP : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) is satisfying_DES1_2 holds
AP : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) is satisfying_DES1_3 ;

theorem :: AFF_3:6
for AP being ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) st AP : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) is satisfying_DES1_2 holds
AP : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) is Desarguesian ;

theorem :: AFF_3:7
for AP being ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) st AP : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) is satisfying_DES2_1 holds
AP : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) is satisfying_DES2 ;

theorem :: AFF_3:8
for AP being ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) holds
( AP : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) is satisfying_DES2_1 iff AP : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) is satisfying_DES2_3 ) ;

theorem :: AFF_3:9
for AP being ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) holds
( AP : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) is satisfying_DES2 iff AP : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) is satisfying_DES2_2 ) ;

theorem :: AFF_3:10
for AP being ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) st AP : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) is satisfying_DES1_3 holds
AP : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) is satisfying_DES2_1 ;