:: AFF_2 semantic presentation

begin

definition
let AP be ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) ;
attr AP is satisfying_PPAP means :: AFF_2:def 1
 for M, N being ( ( ) ( ) Subset of )
for a, b, c, a9, b9, c9 being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st M : ( ( ) ( ) Subset of ) is being_line & N : ( ( ) ( ) Subset of ) is being_line & a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in M : ( ( ) ( ) Subset of ) & b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in M : ( ( ) ( ) Subset of ) & c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in M : ( ( ) ( ) Subset of ) & a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in N : ( ( ) ( ) Subset of ) & b9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in N : ( ( ) ( ) Subset of ) & c9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in N : ( ( ) ( ) Subset of ) & a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) holds
a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ;
end;

definition
let AP be ( ( V46() AffinSpace-like ) ( V41() V46() AffinSpace-like ) AffinSpace) ;
attr AP is Pappian means :: AFF_2:def 2
 for M, N being ( ( ) ( ) Subset of )
for o, a, b, c, a9, b9, c9 being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st M : ( ( ) ( ) Subset of ) is being_line & N : ( ( ) ( ) Subset of ) is being_line & M : ( ( ) ( ) Subset of ) <> N : ( ( ) ( ) Subset of ) & o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in M : ( ( ) ( ) Subset of ) & o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in N : ( ( ) ( ) Subset of ) & o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) <> a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) <> a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) <> b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) <> b9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) <> c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) <> c9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in M : ( ( ) ( ) Subset of ) & b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in M : ( ( ) ( ) Subset of ) & c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in M : ( ( ) ( ) Subset of ) & a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in N : ( ( ) ( ) Subset of ) & b9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in N : ( ( ) ( ) Subset of ) & c9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in N : ( ( ) ( ) Subset of ) & a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) holds
a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a9 : ( ( ) ( ) 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_PAP_1 means :: AFF_2:def 3
 for M, N being ( ( ) ( ) Subset of )
for o, a, b, c, a9, b9, c9 being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st M : ( ( ) ( ) Subset of ) is being_line & N : ( ( ) ( ) Subset of ) is being_line & M : ( ( ) ( ) Subset of ) <> N : ( ( ) ( ) Subset of ) & o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in M : ( ( ) ( ) Subset of ) & o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in N : ( ( ) ( ) Subset of ) & o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) <> a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) <> a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) <> b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) <> b9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) <> c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) <> c9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in M : ( ( ) ( ) Subset of ) & b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in M : ( ( ) ( ) Subset of ) & c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in M : ( ( ) ( ) Subset of ) & b9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in N : ( ( ) ( ) Subset of ) & c9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in N : ( ( ) ( ) Subset of ) & a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) <> c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) holds
a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in N : ( ( ) ( ) Subset of ) ;
end;

definition
let AP be ( ( V46() AffinSpace-like ) ( V41() V46() AffinSpace-like ) AffinSpace) ;
attr AP is Desarguesian means :: AFF_2:def 4
 for A, P, C being ( ( ) ( ) Subset of )
for o, a, b, c, a9, b9, c9 being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in A : ( ( ) ( ) Subset of ) & o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in P : ( ( ) ( ) Subset of ) & o : ( ( ) ( ) 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 ) ) & 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 ) 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 ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b9 : ( ( ) ( ) 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
b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // b9 : ( ( ) ( ) 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_DES_1 means :: AFF_2:def 5
 for A, P, C being ( ( ) ( ) Subset of )
for o, a, b, c, a9, b9, c9 being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in A : ( ( ) ( ) Subset of ) & o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in P : ( ( ) ( ) 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 ) ) & 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 ) 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 ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b9 : ( ( ) ( ) 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 ) ) & b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // b9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & not LIN a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) <> c9 : ( ( ) ( ) 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_DES_2 means :: AFF_2:def 6
 for A, P, C being ( ( ) ( ) Subset of )
for o, a, b, c, a9, b9, c9 being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in A : ( ( ) ( ) Subset of ) & o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in P : ( ( ) ( ) Subset of ) & o : ( ( ) ( ) 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 ) ) & 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 ) & 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 ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b9 : ( ( ) ( ) 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 ) ) & b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // b9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) holds
c9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in C : ( ( ) ( ) Subset of ) ;
end;

definition
let AP be ( ( V46() AffinSpace-like ) ( V41() V46() AffinSpace-like ) AffinSpace) ;
attr AP is Moufangian means :: AFF_2:def 7
 for K being ( ( ) ( ) Subset of )
for o, a, b, c, a9, b9, c9 being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st K : ( ( ) ( ) Subset of ) is being_line & o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in K : ( ( ) ( ) Subset of ) & c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in K : ( ( ) ( ) Subset of ) & c9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in K : ( ( ) ( ) Subset of ) & not a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in K : ( ( ) ( ) Subset of ) & o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) <> c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) <> b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & LIN o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & LIN o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b9 : ( ( ) ( ) 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 ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // K : ( ( ) ( ) Subset of ) holds
b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // b9 : ( ( ) ( ) 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_TDES_1 means :: AFF_2:def 8
 for K being ( ( ) ( ) Subset of )
for o, a, b, c, a9, b9, c9 being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st K : ( ( ) ( ) Subset of ) is being_line & o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in K : ( ( ) ( ) Subset of ) & c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in K : ( ( ) ( ) Subset of ) & c9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in K : ( ( ) ( ) Subset of ) & not a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in K : ( ( ) ( ) Subset of ) & o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) <> c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) <> b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & LIN o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // b9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c9 : ( ( ) ( ) 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 ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // K : ( ( ) ( ) Subset of ) holds
LIN o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b9 : ( ( ) ( ) 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_TDES_2 means :: AFF_2:def 9
 for K being ( ( ) ( ) Subset of )
for o, a, b, c, a9, b9, c9 being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st K : ( ( ) ( ) Subset of ) is being_line & o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in K : ( ( ) ( ) Subset of ) & c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in K : ( ( ) ( ) Subset of ) & c9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in K : ( ( ) ( ) Subset of ) & not a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in K : ( ( ) ( ) Subset of ) & o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) <> c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) <> b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & LIN o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & LIN o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // b9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c9 : ( ( ) ( ) 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 ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // K : ( ( ) ( ) Subset of ) holds
a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b9 : ( ( ) ( ) 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_TDES_3 means :: AFF_2:def 10
 for K being ( ( ) ( ) Subset of )
for o, a, b, c, a9, b9, c9 being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st K : ( ( ) ( ) Subset of ) is being_line & o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in K : ( ( ) ( ) Subset of ) & c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in K : ( ( ) ( ) Subset of ) & not a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in K : ( ( ) ( ) Subset of ) & o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) <> c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) <> b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & LIN o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & LIN o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b9 : ( ( ) ( ) 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 ) ) & b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // b9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // K : ( ( ) ( ) Subset of ) holds
c9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in K : ( ( ) ( ) Subset of ) ;
end;

definition
let AP be ( ( V46() AffinSpace-like ) ( V41() V46() AffinSpace-like ) AffinSpace) ;
attr AP is translational means :: AFF_2:def 11
 for A, P, C being ( ( ) ( ) Subset of )
for a, b, c, a9, b9, c9 being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st A : ( ( ) ( ) Subset of ) // P : ( ( ) ( ) Subset of ) & A : ( ( ) ( ) 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 ) 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 ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b9 : ( ( ) ( ) 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
b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // b9 : ( ( ) ( ) 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_des_1 means :: AFF_2:def 12
 for A, P, C being ( ( ) ( ) Subset of )
for a, b, c, a9, b9, c9 being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st A : ( ( ) ( ) Subset of ) // P : ( ( ) ( ) 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 ) 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 ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b9 : ( ( ) ( ) 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 ) ) & b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // b9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & not LIN a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) <> c9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) holds
A : ( ( ) ( ) Subset of ) // C : ( ( ) ( ) Subset of ) ;
end;

definition
let AP be ( ( V46() AffinSpace-like ) ( V41() V46() AffinSpace-like ) AffinSpace) ;
attr AP is satisfying_pap means :: AFF_2:def 13
 for M, N being ( ( ) ( ) Subset of )
for a, b, c, a9, b9, c9 being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st M : ( ( ) ( ) Subset of ) is being_line & N : ( ( ) ( ) Subset of ) is being_line & a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in M : ( ( ) ( ) Subset of ) & b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in M : ( ( ) ( ) Subset of ) & c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in M : ( ( ) ( ) Subset of ) & M : ( ( ) ( ) Subset of ) // N : ( ( ) ( ) Subset of ) & M : ( ( ) ( ) Subset of ) <> N : ( ( ) ( ) Subset of ) & a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in N : ( ( ) ( ) Subset of ) & b9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in N : ( ( ) ( ) Subset of ) & c9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in N : ( ( ) ( ) Subset of ) & a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) holds
a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a9 : ( ( ) ( ) 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_pap_1 means :: AFF_2:def 14
 for M, N being ( ( ) ( ) Subset of )
for a, b, c, a9, b9, c9 being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st M : ( ( ) ( ) Subset of ) is being_line & N : ( ( ) ( ) Subset of ) is being_line & a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in M : ( ( ) ( ) Subset of ) & b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in M : ( ( ) ( ) Subset of ) & c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in M : ( ( ) ( ) Subset of ) & M : ( ( ) ( ) Subset of ) // N : ( ( ) ( ) Subset of ) & M : ( ( ) ( ) Subset of ) <> N : ( ( ) ( ) Subset of ) & a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in N : ( ( ) ( ) Subset of ) & b9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in N : ( ( ) ( ) Subset of ) & a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) <> b9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) holds
c9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in N : ( ( ) ( ) Subset of ) ;
end;

theorem :: AFF_2:1
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 Pappian iff AP : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) is satisfying_PAP_1 ) ;

theorem :: AFF_2:2
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 Desarguesian iff AP : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) is satisfying_DES_1 ) ;

theorem :: AFF_2: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 Moufangian holds
AP : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) is satisfying_TDES_1 ;

theorem :: AFF_2: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 satisfying_TDES_1 holds
AP : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) is satisfying_TDES_2 ;

theorem :: AFF_2: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_TDES_2 holds
AP : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) is satisfying_TDES_3 ;

theorem :: AFF_2: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_TDES_3 holds
AP : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) is Moufangian ;

theorem :: AFF_2:7
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 translational iff AP : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) is satisfying_des_1 ) ;

theorem :: AFF_2: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_pap iff AP : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) is satisfying_pap_1 ) ;

theorem :: AFF_2:9
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 Pappian holds
AP : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) is satisfying_pap ;

theorem :: AFF_2:10
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_PPAP iff ( AP : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) is Pappian & AP : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) is satisfying_pap ) ) ;

theorem :: AFF_2:11
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 Pappian holds
AP : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) is Desarguesian ;

theorem :: AFF_2:12
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 Moufangian ;

theorem :: AFF_2:13
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_TDES_1 holds
AP : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) is satisfying_des_1 ;

theorem :: AFF_2:14
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 Moufangian holds
AP : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) is translational ;

theorem :: AFF_2:15
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 translational holds
AP : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) is satisfying_pap ;