:: CONMETR1 semantic presentation

begin

definition
let X be ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) ;
attr X is satisfying_minor_Scherungssatz means :: CONMETR1:def 1
 for a1, a2, a3, a4, b1, b2, b3, b4 being ( ( ) ( ) Element of ( ( ) ( ) set ) )
for M, N being ( ( ) ( ) Subset of ) st M : ( ( ) ( ) Subset of ) // N : ( ( ) ( ) Subset of ) & a1 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in M : ( ( ) ( ) Subset of ) & a3 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in M : ( ( ) ( ) Subset of ) & b1 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in M : ( ( ) ( ) Subset of ) & b3 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in M : ( ( ) ( ) Subset of ) & a2 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in N : ( ( ) ( ) Subset of ) & a4 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in N : ( ( ) ( ) Subset of ) & b2 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in N : ( ( ) ( ) Subset of ) & b4 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in N : ( ( ) ( ) Subset of ) & not a4 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in M : ( ( ) ( ) Subset of ) & not a2 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in M : ( ( ) ( ) Subset of ) & not b2 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in M : ( ( ) ( ) Subset of ) & not b4 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in M : ( ( ) ( ) Subset of ) & not a1 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in N : ( ( ) ( ) Subset of ) & not a3 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in N : ( ( ) ( ) Subset of ) & not b1 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in N : ( ( ) ( ) Subset of ) & not b3 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in N : ( ( ) ( ) Subset of ) & a3 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a2 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // b3 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b2 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & a2 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a1 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // b2 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b1 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & a1 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a4 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // b1 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b4 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) holds
a3 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a4 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // b3 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b4 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ;
end;

definition
let X be ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) ;
attr X is satisfying_major_Scherungssatz means :: CONMETR1:def 2
 for o, a1, a2, a3, a4, b1, b2, b3, b4 being ( ( ) ( ) Element of ( ( ) ( ) set ) )
for M, N being ( ( ) ( ) Subset of ) st M : ( ( ) ( ) Subset of ) is being_line & N : ( ( ) ( ) Subset of ) is being_line & o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in M : ( ( ) ( ) Subset of ) & o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in N : ( ( ) ( ) Subset of ) & a1 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in M : ( ( ) ( ) Subset of ) & a3 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in M : ( ( ) ( ) Subset of ) & b1 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in M : ( ( ) ( ) Subset of ) & b3 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in M : ( ( ) ( ) Subset of ) & a2 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in N : ( ( ) ( ) Subset of ) & a4 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in N : ( ( ) ( ) Subset of ) & b2 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in N : ( ( ) ( ) Subset of ) & b4 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in N : ( ( ) ( ) Subset of ) & not a4 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in M : ( ( ) ( ) Subset of ) & not a2 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in M : ( ( ) ( ) Subset of ) & not b2 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in M : ( ( ) ( ) Subset of ) & not b4 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in M : ( ( ) ( ) Subset of ) & not a1 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in N : ( ( ) ( ) Subset of ) & not a3 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in N : ( ( ) ( ) Subset of ) & not b1 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in N : ( ( ) ( ) Subset of ) & not b3 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in N : ( ( ) ( ) Subset of ) & a3 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a2 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // b3 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b2 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & a2 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a1 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // b2 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b1 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & a1 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a4 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // b1 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b4 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) holds
a3 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a4 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // b3 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b4 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ;
end;

definition
let X be ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) ;
attr X is satisfying_Scherungssatz means :: CONMETR1:def 3
 for a1, a2, a3, a4, b1, b2, b3, b4 being ( ( ) ( ) Element of ( ( ) ( ) set ) )
for M, N being ( ( ) ( ) Subset of ) st M : ( ( ) ( ) Subset of ) is being_line & N : ( ( ) ( ) Subset of ) is being_line & a1 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in M : ( ( ) ( ) Subset of ) & a3 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in M : ( ( ) ( ) Subset of ) & b1 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in M : ( ( ) ( ) Subset of ) & b3 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in M : ( ( ) ( ) Subset of ) & a2 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in N : ( ( ) ( ) Subset of ) & a4 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in N : ( ( ) ( ) Subset of ) & b2 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in N : ( ( ) ( ) Subset of ) & b4 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in N : ( ( ) ( ) Subset of ) & not a4 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in M : ( ( ) ( ) Subset of ) & not a2 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in M : ( ( ) ( ) Subset of ) & not b2 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in M : ( ( ) ( ) Subset of ) & not b4 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in M : ( ( ) ( ) Subset of ) & not a1 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in N : ( ( ) ( ) Subset of ) & not a3 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in N : ( ( ) ( ) Subset of ) & not b1 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in N : ( ( ) ( ) Subset of ) & not b3 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in N : ( ( ) ( ) Subset of ) & a3 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a2 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // b3 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b2 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & a2 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a1 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // b2 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b1 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & a1 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a4 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // b1 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b4 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) holds
a3 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a4 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // b3 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b4 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ;
end;

definition
let X be ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) ;
attr X is satisfying_indirect_Scherungssatz means :: CONMETR1:def 4
 for a1, a2, a3, a4, b1, b2, b3, b4 being ( ( ) ( ) Element of ( ( ) ( ) set ) )
for M, N being ( ( ) ( ) Subset of ) st M : ( ( ) ( ) Subset of ) is being_line & N : ( ( ) ( ) Subset of ) is being_line & a1 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in M : ( ( ) ( ) Subset of ) & a3 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in M : ( ( ) ( ) Subset of ) & b2 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in M : ( ( ) ( ) Subset of ) & b4 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in M : ( ( ) ( ) Subset of ) & a2 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in N : ( ( ) ( ) Subset of ) & a4 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in N : ( ( ) ( ) Subset of ) & b1 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in N : ( ( ) ( ) Subset of ) & b3 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in N : ( ( ) ( ) Subset of ) & not a4 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in M : ( ( ) ( ) Subset of ) & not a2 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in M : ( ( ) ( ) Subset of ) & not b1 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in M : ( ( ) ( ) Subset of ) & not b3 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in M : ( ( ) ( ) Subset of ) & not a1 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in N : ( ( ) ( ) Subset of ) & not a3 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in N : ( ( ) ( ) Subset of ) & not b2 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in N : ( ( ) ( ) Subset of ) & not b4 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in N : ( ( ) ( ) Subset of ) & a3 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a2 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // b3 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b2 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & a2 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a1 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // b2 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b1 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & a1 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a4 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // b1 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b4 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) holds
a3 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a4 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // b3 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b4 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ;
end;

definition
let X be ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) ;
attr X is satisfying_minor_indirect_Scherungssatz means :: CONMETR1:def 5
 for a1, a2, a3, a4, b1, b2, b3, b4 being ( ( ) ( ) Element of ( ( ) ( ) set ) )
for M, N being ( ( ) ( ) Subset of ) st M : ( ( ) ( ) Subset of ) // N : ( ( ) ( ) Subset of ) & a1 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in M : ( ( ) ( ) Subset of ) & a3 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in M : ( ( ) ( ) Subset of ) & b2 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in M : ( ( ) ( ) Subset of ) & b4 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in M : ( ( ) ( ) Subset of ) & a2 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in N : ( ( ) ( ) Subset of ) & a4 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in N : ( ( ) ( ) Subset of ) & b1 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in N : ( ( ) ( ) Subset of ) & b3 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in N : ( ( ) ( ) Subset of ) & not a4 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in M : ( ( ) ( ) Subset of ) & not a2 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in M : ( ( ) ( ) Subset of ) & not b1 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in M : ( ( ) ( ) Subset of ) & not b3 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in M : ( ( ) ( ) Subset of ) & not a1 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in N : ( ( ) ( ) Subset of ) & not a3 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in N : ( ( ) ( ) Subset of ) & not b2 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in N : ( ( ) ( ) Subset of ) & not b4 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in N : ( ( ) ( ) Subset of ) & a3 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a2 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // b3 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b2 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & a2 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a1 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // b2 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b1 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & a1 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a4 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // b1 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b4 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) holds
a3 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a4 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // b3 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b4 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ;
end;

definition
let X be ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) ;
attr X is satisfying_major_indirect_Scherungssatz means :: CONMETR1:def 6
 for o, a1, a2, a3, a4, b1, b2, b3, b4 being ( ( ) ( ) Element of ( ( ) ( ) set ) )
for M, N being ( ( ) ( ) Subset of ) st M : ( ( ) ( ) Subset of ) is being_line & N : ( ( ) ( ) Subset of ) is being_line & o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in M : ( ( ) ( ) Subset of ) & o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in N : ( ( ) ( ) Subset of ) & a1 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in M : ( ( ) ( ) Subset of ) & a3 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in M : ( ( ) ( ) Subset of ) & b2 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in M : ( ( ) ( ) Subset of ) & b4 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in M : ( ( ) ( ) Subset of ) & a2 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in N : ( ( ) ( ) Subset of ) & a4 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in N : ( ( ) ( ) Subset of ) & b1 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in N : ( ( ) ( ) Subset of ) & b3 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in N : ( ( ) ( ) Subset of ) & not a4 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in M : ( ( ) ( ) Subset of ) & not a2 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in M : ( ( ) ( ) Subset of ) & not b1 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in M : ( ( ) ( ) Subset of ) & not b3 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in M : ( ( ) ( ) Subset of ) & not a1 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in N : ( ( ) ( ) Subset of ) & not a3 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in N : ( ( ) ( ) Subset of ) & not b2 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in N : ( ( ) ( ) Subset of ) & not b4 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) in N : ( ( ) ( ) Subset of ) & a3 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a2 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // b3 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b2 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & a2 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a1 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // b2 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b1 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & a1 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a4 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // b1 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b4 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) holds
a3 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a4 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // b3 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b4 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ;
end;

theorem :: CONMETR1:1
for X being ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) holds
( X : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) is satisfying_indirect_Scherungssatz iff ( X : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) is satisfying_minor_indirect_Scherungssatz & X : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) is satisfying_major_indirect_Scherungssatz ) ) ;

theorem :: CONMETR1:2
for X being ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) holds
( X : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) is satisfying_Scherungssatz iff ( X : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) is satisfying_minor_Scherungssatz & X : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) is satisfying_major_Scherungssatz ) ) ;

theorem :: CONMETR1:3
for X being ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) st X : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) is satisfying_minor_indirect_Scherungssatz holds
X : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) is satisfying_minor_Scherungssatz ;

theorem :: CONMETR1:4
for X being ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) st X : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) is satisfying_major_indirect_Scherungssatz holds
X : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) is satisfying_major_Scherungssatz ;

theorem :: CONMETR1:5
for X being ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) st X : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) is satisfying_indirect_Scherungssatz holds
X : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) is satisfying_Scherungssatz ;

theorem :: CONMETR1:6
for X being ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) st X : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) is translational holds
X : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) is satisfying_minor_Scherungssatz ;

theorem :: CONMETR1:7
for X being ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) st X : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) is Desarguesian holds
X : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) is satisfying_major_Scherungssatz ;

theorem :: CONMETR1:8
for X being ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) holds
( X : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) is Desarguesian iff X : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) is satisfying_Scherungssatz ) ;

theorem :: CONMETR1:9
for X being ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) holds
( X : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) is satisfying_pap iff X : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) is satisfying_minor_indirect_Scherungssatz ) ;

theorem :: CONMETR1:10
for X being ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) holds
( X : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) is Pappian iff X : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) is satisfying_major_indirect_Scherungssatz ) ;

theorem :: CONMETR1:11
for X being ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) holds
( X : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) is satisfying_PPAP iff X : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) is satisfying_indirect_Scherungssatz ) ;

theorem :: CONMETR1:12
for X being ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) st X : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) is satisfying_major_indirect_Scherungssatz holds
X : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) is satisfying_minor_indirect_Scherungssatz ;

theorem :: CONMETR1:13
for X being ( ( V41() OrtAfPl-like ) ( V41() OrtAfSp-like OrtAfPl-like ) OrtAfPl) holds
( Af X : ( ( V41() OrtAfPl-like ) ( V41() OrtAfSp-like OrtAfPl-like ) OrtAfPl) : ( ( strict ) ( V41() V46() strict AffinSpace-like 2-dimensional ) AffinStruct ) is satisfying_Scherungssatz iff X : ( ( V41() OrtAfPl-like ) ( V41() OrtAfSp-like OrtAfPl-like ) OrtAfPl) is satisfying_SCH ) ;

theorem :: CONMETR1:14
for X being ( ( V41() OrtAfPl-like ) ( V41() OrtAfSp-like OrtAfPl-like ) OrtAfPl) holds
( X : ( ( V41() OrtAfPl-like ) ( V41() OrtAfSp-like OrtAfPl-like ) OrtAfPl) is satisfying_TDES iff Af X : ( ( V41() OrtAfPl-like ) ( V41() OrtAfSp-like OrtAfPl-like ) OrtAfPl) : ( ( strict ) ( V41() V46() strict AffinSpace-like 2-dimensional ) AffinStruct ) is Moufangian ) ;

theorem :: CONMETR1:15
for X being ( ( V41() OrtAfPl-like ) ( V41() OrtAfSp-like OrtAfPl-like ) OrtAfPl) holds
( Af X : ( ( V41() OrtAfPl-like ) ( V41() OrtAfSp-like OrtAfPl-like ) OrtAfPl) : ( ( strict ) ( V41() V46() strict AffinSpace-like 2-dimensional ) AffinStruct ) is translational iff X : ( ( V41() OrtAfPl-like ) ( V41() OrtAfSp-like OrtAfPl-like ) OrtAfPl) is satisfying_des ) ;

theorem :: CONMETR1:16
for X being ( ( V41() OrtAfPl-like ) ( V41() OrtAfSp-like OrtAfPl-like ) OrtAfPl) holds
( X : ( ( V41() OrtAfPl-like ) ( V41() OrtAfSp-like OrtAfPl-like ) OrtAfPl) is satisfying_PAP iff Af X : ( ( V41() OrtAfPl-like ) ( V41() OrtAfSp-like OrtAfPl-like ) OrtAfPl) : ( ( strict ) ( V41() V46() strict AffinSpace-like 2-dimensional ) AffinStruct ) is Pappian ) ;

theorem :: CONMETR1:17
for X being ( ( V41() OrtAfPl-like ) ( V41() OrtAfSp-like OrtAfPl-like ) OrtAfPl) holds
( X : ( ( V41() OrtAfPl-like ) ( V41() OrtAfSp-like OrtAfPl-like ) OrtAfPl) is satisfying_DES iff Af X : ( ( V41() OrtAfPl-like ) ( V41() OrtAfSp-like OrtAfPl-like ) OrtAfPl) : ( ( strict ) ( V41() V46() strict AffinSpace-like 2-dimensional ) AffinStruct ) is Desarguesian ) ;