ARROW

:: ARROW semantic presentation

definition

let A, B9 be ( ( non empty ) ( non empty ) set ) ;
let B be ( ( non empty ) ( non empty ) Subset of ( ( ) ( ) set ) ) ;
let f be ( ( Function-like quasi_total ) ( Relation-like A : ( ( non empty ) ( non empty ) set ) -defined B : ( ( non empty ) ( non empty ) Subset of ( ( ) ( ) set ) ) -valued Function-like quasi_total ) Function of A : ( ( non empty ) ( non empty ) set ) ,B : ( ( non empty ) ( non empty ) Subset of ( ( ) ( ) set ) ) ) ;
let x be ( ( ) ( ) Element of A : ( ( non empty ) ( non empty ) set ) ) ;
:: original: .
redefine func f . x -> ( ( ) ( ) Element of B : ( ( ) ( Relation-like Function-like FinSequence-like ) FinSequence of A : ( ( Relation-like ) ( Relation-like ) set ) ) ) ;

end;

theorem :: ARROW:1

for A being ( ( finite ) ( finite ) set ) st card A : ( ( finite ) ( finite ) set ) : ( ( ) ( ext-real non negative V24() V25() V26() V30() V31() V32() V44() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) set ) ) >= 2 : ( ( ) ( ext-real positive non negative non empty V24() V25() V26() V30() V31() V32() V44() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) holds
for a being ( ( ) ( ) Element of A : ( ( finite ) ( finite ) set ) ) ex b being ( ( ) ( ) Element of A : ( ( finite ) ( finite ) set ) ) st b : ( ( ) ( ) Element of b₁ : ( ( finite ) ( finite ) set ) ) <> a : ( ( ) ( ) Element of b₁ : ( ( finite ) ( finite ) set ) ) ;

theorem :: ARROW:2

for A being ( ( finite ) ( finite ) set ) st card A : ( ( finite ) ( finite ) set ) : ( ( ) ( ext-real non negative V24() V25() V26() V30() V31() V32() V44() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) set ) ) >= 3 : ( ( ) ( ext-real positive non negative non empty V24() V25() V26() V30() V31() V32() V44() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) holds
for a, b being ( ( ) ( ) Element of A : ( ( finite ) ( finite ) set ) ) ex c being ( ( ) ( ) Element of A : ( ( finite ) ( finite ) set ) ) st
( c : ( ( ) ( ) Element of b₁ : ( ( finite ) ( finite ) set ) ) <> a : ( ( ) ( ) Element of b₁ : ( ( finite ) ( finite ) set ) ) & c : ( ( ) ( ) Element of b₁ : ( ( finite ) ( finite ) set ) ) <> b : ( ( ) ( ) Element of b₁ : ( ( finite ) ( finite ) set ) ) ) ;

definition

let A be ( ( non empty ) ( non empty ) set ) ;

func LinPreorders A -> ( ( ) ( ) set ) means :: ARROW:def 1
for R being ( ( ) ( ) set ) holds
( R : ( ( ) ( ) set ) in it : ( ( Relation-like ) ( Relation-like ) set ) iff ( R : ( ( ) ( ) set ) is ( ( ) ( Relation-like A : ( ( Relation-like ) ( Relation-like ) set ) -defined A : ( ( Relation-like ) ( Relation-like ) set ) -valued ) Relation of ) & ( for a, b being ( ( ) ( ) Element of A : ( ( Relation-like ) ( Relation-like ) set ) ) holds
( [a : ( ( ) ( ) Element of A : ( ( non empty ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of A : ( ( non empty ) ( non empty ) set ) ) ] : ( ( ) ( ) set ) in R : ( ( ) ( ) set ) or [b : ( ( ) ( ) Element of A : ( ( non empty ) ( non empty ) set ) ) ,a : ( ( ) ( ) Element of A : ( ( non empty ) ( non empty ) set ) ) ] : ( ( ) ( ) set ) in R : ( ( ) ( ) set ) ) ) & ( for a, b, c being ( ( ) ( ) Element of A : ( ( Relation-like ) ( Relation-like ) set ) ) st [a : ( ( ) ( ) Element of A : ( ( non empty ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of A : ( ( non empty ) ( non empty ) set ) ) ] : ( ( ) ( ) set ) in R : ( ( ) ( ) set ) & [b : ( ( ) ( ) Element of A : ( ( non empty ) ( non empty ) set ) ) ,c : ( ( ) ( ) Element of A : ( ( non empty ) ( non empty ) set ) ) ] : ( ( ) ( ) set ) in R : ( ( ) ( ) set ) holds
[a : ( ( ) ( ) Element of A : ( ( non empty ) ( non empty ) set ) ) ,c : ( ( ) ( ) Element of A : ( ( non empty ) ( non empty ) set ) ) ] : ( ( ) ( ) set ) in R : ( ( ) ( ) set ) ) ) );

end;

registration

let A be ( ( non empty ) ( non empty ) set ) ;

cluster LinPreorders A : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) -> non empty ;

end;

definition

let A be ( ( non empty ) ( non empty ) set ) ;

func LinOrders A -> ( ( ) ( ) Subset of ( ( ) ( ) set ) ) means :: ARROW:def 2
for R being ( ( ) ( ) Element of LinPreorders A : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) holds
( R : ( ( ) ( ) Element of LinPreorders A : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) in it : ( ( non empty ) ( non empty ) set ) iff for a, b being ( ( ) ( ) Element of A : ( ( ) ( ) set ) ) st [a : ( ( ) ( ) Element of A : ( ( non empty ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of A : ( ( non empty ) ( non empty ) set ) ) ] : ( ( ) ( ) set ) in R : ( ( ) ( ) Element of LinPreorders A : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) & [b : ( ( ) ( ) Element of A : ( ( non empty ) ( non empty ) set ) ) ,a : ( ( ) ( ) Element of A : ( ( non empty ) ( non empty ) set ) ) ] : ( ( ) ( ) set ) in R : ( ( ) ( ) Element of LinPreorders A : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) holds
a : ( ( ) ( ) Element of A : ( ( non empty ) ( non empty ) set ) ) = b : ( ( ) ( ) Element of A : ( ( non empty ) ( non empty ) set ) ) );

end;

registration

let A be ( ( ) ( ) set ) ;

cluster Relation-like A : ( ( ) ( ) set ) -defined A : ( ( ) ( ) set ) -valued V17(A : ( ( ) ( ) set ) ) reflexive antisymmetric connected transitive for ( ( ) ( ) Element of bool [:A : ( ( ) ( ) set ) ,A : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ;

end;

definition

let A be ( ( non empty ) ( non empty ) set ) ;

redefine func LinOrders A means :: ARROW:def 3
for R being ( ( ) ( ) set ) holds
( R : ( ( ) ( ) set ) in it : ( ( non empty ) ( non empty ) set ) iff R : ( ( ) ( ) set ) is ( ( V17(A : ( ( ) ( ) set ) ) reflexive antisymmetric connected transitive ) ( Relation-like A : ( ( ) ( ) set ) -defined A : ( ( ) ( ) set ) -valued V17(A : ( ( ) ( ) set ) ) reflexive antisymmetric connected transitive ) Order of ) );

end;

registration

let A be ( ( non empty ) ( non empty ) set ) ;

cluster LinOrders A : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) -> non empty ;

end;

registration

let A be ( ( non empty ) ( non empty ) set ) ;

cluster -> Relation-like for ( ( ) ( ) Element of LinPreorders A : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ;

cluster -> Relation-like for ( ( ) ( ) Element of LinOrders A : ( ( ) ( ) set ) : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) ) ;

end;

definition

let o be ( ( Relation-like ) ( Relation-like ) Relation) ;
let a, b be ( ( ) ( ) set ) ;

pred a <=_ o,b means :: ARROW:def 4
[a : ( ( non empty ) ( non empty ) set ) ,b : ( ( ) ( Relation-like Function-like FinSequence-like ) FinSequence of o : ( ( ) ( ) set ) ) ] : ( ( ) ( ) set ) in o : ( ( ) ( ) set ) ;

end;

notation

let o be ( ( Relation-like ) ( Relation-like ) Relation) ;
let a, b be ( ( ) ( ) set ) ;
synonym b >=_ o,a for a <=_ o,b;
antonym b <_ o,a for a <=_ o,b;
antonym a >_ o,b for a <=_ o,b;

end;

theorem :: ARROW:3

for A being ( ( non empty ) ( non empty ) set )
for a being ( ( ) ( ) Element of A : ( ( non empty ) ( non empty ) set ) )
for o being ( ( ) ( Relation-like ) Element of LinPreorders A : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) holds a : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) <=_ o : ( ( ) ( Relation-like ) Element of LinPreorders b₁ : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,a : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) ;

theorem :: ARROW:4

for A being ( ( non empty ) ( non empty ) set )
for a, b being ( ( ) ( ) Element of A : ( ( non empty ) ( non empty ) set ) )
for o being ( ( ) ( Relation-like ) Element of LinPreorders A : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) holds
( a : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) <=_ o : ( ( ) ( Relation-like ) Element of LinPreorders b₁ : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) or b : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) <=_ o : ( ( ) ( Relation-like ) Element of LinPreorders b₁ : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,a : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) ) ;

theorem :: ARROW:5

for A being ( ( non empty ) ( non empty ) set )
for a, b, c being ( ( ) ( ) Element of A : ( ( non empty ) ( non empty ) set ) )
for o being ( ( ) ( Relation-like ) Element of LinPreorders A : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) st ( a : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) <=_ o : ( ( ) ( Relation-like ) Element of LinPreorders b₁ : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) or a : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) <_ o : ( ( ) ( Relation-like ) Element of LinPreorders b₁ : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) ) & ( b : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) <=_ o : ( ( ) ( Relation-like ) Element of LinPreorders b₁ : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) or b : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) <_ o : ( ( ) ( Relation-like ) Element of LinPreorders b₁ : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) ) holds
a : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) <=_ o : ( ( ) ( Relation-like ) Element of LinPreorders b₁ : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) ;

theorem :: ARROW:6

for A being ( ( non empty ) ( non empty ) set )
for a, b being ( ( ) ( ) Element of A : ( ( non empty ) ( non empty ) set ) )
for o99 being ( ( ) ( Relation-like ) Element of LinOrders A : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Subset of ( ( ) ( ) set ) ) ) st a : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) <=_ o99 : ( ( ) ( Relation-like ) Element of LinOrders b₁ : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Subset of ( ( ) ( ) set ) ) ) ,b : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) & b : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) <=_ o99 : ( ( ) ( Relation-like ) Element of LinOrders b₁ : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Subset of ( ( ) ( ) set ) ) ) ,a : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) holds
a : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) = b : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) ;

theorem :: ARROW:7

for A being ( ( non empty ) ( non empty ) set )
for a, b, c being ( ( ) ( ) Element of A : ( ( non empty ) ( non empty ) set ) ) st a : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) <> b : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) & b : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) <> c : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) & a : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) <> c : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) holds
ex o being ( ( ) ( Relation-like ) Element of LinPreorders A : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) st
( a : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) <_ o : ( ( ) ( Relation-like ) Element of LinPreorders b₁ : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) & b : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) <_ o : ( ( ) ( Relation-like ) Element of LinPreorders b₁ : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) ) ;

theorem :: ARROW:8

for A being ( ( non empty ) ( non empty ) set )
for b being ( ( ) ( ) Element of A : ( ( non empty ) ( non empty ) set ) ) ex o being ( ( ) ( Relation-like ) Element of LinPreorders A : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) st
for a being ( ( ) ( ) Element of A : ( ( non empty ) ( non empty ) set ) ) st a : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) <> b : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) holds
b : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) <_ o : ( ( ) ( Relation-like ) Element of LinPreorders b₁ : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,a : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) ;

theorem :: ARROW:9

for A being ( ( non empty ) ( non empty ) set )
for b being ( ( ) ( ) Element of A : ( ( non empty ) ( non empty ) set ) ) ex o being ( ( ) ( Relation-like ) Element of LinPreorders A : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) st
for a being ( ( ) ( ) Element of A : ( ( non empty ) ( non empty ) set ) ) st a : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) <> b : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) holds
a : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) <_ o : ( ( ) ( Relation-like ) Element of LinPreorders b₁ : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) ;

theorem :: ARROW:10

for A being ( ( non empty ) ( non empty ) set )
for a, b, c being ( ( ) ( ) Element of A : ( ( non empty ) ( non empty ) set ) )
for o9 being ( ( ) ( Relation-like ) Element of LinPreorders A : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) st a : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) <> b : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) & a : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) <> c : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) holds
ex o being ( ( ) ( Relation-like ) Element of LinPreorders A : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) st
( a : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) <_ o : ( ( ) ( Relation-like ) Element of LinPreorders b₁ : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) & a : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) <_ o : ( ( ) ( Relation-like ) Element of LinPreorders b₁ : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) & ( b : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) <_ o : ( ( ) ( Relation-like ) Element of LinPreorders b₁ : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) implies b : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) <_ o9 : ( ( ) ( Relation-like ) Element of LinPreorders b₁ : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) ) & ( b : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) <_ o9 : ( ( ) ( Relation-like ) Element of LinPreorders b₁ : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) implies b : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) <_ o : ( ( ) ( Relation-like ) Element of LinPreorders b₁ : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) ) & ( c : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) <_ o : ( ( ) ( Relation-like ) Element of LinPreorders b₁ : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) implies c : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) <_ o9 : ( ( ) ( Relation-like ) Element of LinPreorders b₁ : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) ) & ( c : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) <_ o9 : ( ( ) ( Relation-like ) Element of LinPreorders b₁ : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) implies c : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) <_ o : ( ( ) ( Relation-like ) Element of LinPreorders b₁ : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) ) ) ;

theorem :: ARROW:11

for A being ( ( non empty ) ( non empty ) set )
for a, b, c being ( ( ) ( ) Element of A : ( ( non empty ) ( non empty ) set ) )
for o9 being ( ( ) ( Relation-like ) Element of LinPreorders A : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) st a : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) <> b : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) & a : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) <> c : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) holds
ex o being ( ( ) ( Relation-like ) Element of LinPreorders A : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) st
( b : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) <_ o : ( ( ) ( Relation-like ) Element of LinPreorders b₁ : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,a : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) & c : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) <_ o : ( ( ) ( Relation-like ) Element of LinPreorders b₁ : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,a : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) & ( b : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) <_ o : ( ( ) ( Relation-like ) Element of LinPreorders b₁ : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) implies b : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) <_ o9 : ( ( ) ( Relation-like ) Element of LinPreorders b₁ : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) ) & ( b : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) <_ o9 : ( ( ) ( Relation-like ) Element of LinPreorders b₁ : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) implies b : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) <_ o : ( ( ) ( Relation-like ) Element of LinPreorders b₁ : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) ) & ( c : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) <_ o : ( ( ) ( Relation-like ) Element of LinPreorders b₁ : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) implies c : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) <_ o9 : ( ( ) ( Relation-like ) Element of LinPreorders b₁ : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) ) & ( c : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) <_ o9 : ( ( ) ( Relation-like ) Element of LinPreorders b₁ : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) implies c : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) <_ o : ( ( ) ( Relation-like ) Element of LinPreorders b₁ : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) ) ) ;

theorem :: ARROW:12

for A being ( ( non empty ) ( non empty ) set )
for a, b being ( ( ) ( ) Element of A : ( ( non empty ) ( non empty ) set ) )
for o, o9 being ( ( ) ( Relation-like ) Element of LinOrders A : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Subset of ( ( ) ( ) set ) ) ) holds
( not ( ( a : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) <_ o : ( ( ) ( Relation-like ) Element of LinOrders b₁ : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Subset of ( ( ) ( ) set ) ) ) ,b : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) implies a : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) <_ o9 : ( ( ) ( Relation-like ) Element of LinOrders b₁ : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Subset of ( ( ) ( ) set ) ) ) ,b : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) ) & ( a : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) <_ o9 : ( ( ) ( Relation-like ) Element of LinOrders b₁ : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Subset of ( ( ) ( ) set ) ) ) ,b : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) implies a : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) <_ o : ( ( ) ( Relation-like ) Element of LinOrders b₁ : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Subset of ( ( ) ( ) set ) ) ) ,b : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) ) & ( b : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) <_ o : ( ( ) ( Relation-like ) Element of LinOrders b₁ : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Subset of ( ( ) ( ) set ) ) ) ,a : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) implies b : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) <_ o9 : ( ( ) ( Relation-like ) Element of LinOrders b₁ : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Subset of ( ( ) ( ) set ) ) ) ,a : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) ) & ( b : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) <_ o9 : ( ( ) ( Relation-like ) Element of LinOrders b₁ : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Subset of ( ( ) ( ) set ) ) ) ,a : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) implies b : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) <_ o : ( ( ) ( Relation-like ) Element of LinOrders b₁ : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Subset of ( ( ) ( ) set ) ) ) ,a : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) ) & not ( a : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) <_ o : ( ( ) ( Relation-like ) Element of LinOrders b₁ : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Subset of ( ( ) ( ) set ) ) ) ,b : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) iff a : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) <_ o9 : ( ( ) ( Relation-like ) Element of LinOrders b₁ : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Subset of ( ( ) ( ) set ) ) ) ,b : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) ) ) & not ( ( a : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) <_ o : ( ( ) ( Relation-like ) Element of LinOrders b₁ : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Subset of ( ( ) ( ) set ) ) ) ,b : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) implies a : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) <_ o9 : ( ( ) ( Relation-like ) Element of LinOrders b₁ : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Subset of ( ( ) ( ) set ) ) ) ,b : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) ) & ( a : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) <_ o9 : ( ( ) ( Relation-like ) Element of LinOrders b₁ : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Subset of ( ( ) ( ) set ) ) ) ,b : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) implies a : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) <_ o : ( ( ) ( Relation-like ) Element of LinOrders b₁ : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Subset of ( ( ) ( ) set ) ) ) ,b : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) ) & not ( ( a : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) <_ o : ( ( ) ( Relation-like ) Element of LinOrders b₁ : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Subset of ( ( ) ( ) set ) ) ) ,b : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) implies a : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) <_ o9 : ( ( ) ( Relation-like ) Element of LinOrders b₁ : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Subset of ( ( ) ( ) set ) ) ) ,b : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) ) & ( a : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) <_ o9 : ( ( ) ( Relation-like ) Element of LinOrders b₁ : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Subset of ( ( ) ( ) set ) ) ) ,b : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) implies a : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) <_ o : ( ( ) ( Relation-like ) Element of LinOrders b₁ : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Subset of ( ( ) ( ) set ) ) ) ,b : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) ) & ( b : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) <_ o : ( ( ) ( Relation-like ) Element of LinOrders b₁ : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Subset of ( ( ) ( ) set ) ) ) ,a : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) implies b : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) <_ o9 : ( ( ) ( Relation-like ) Element of LinOrders b₁ : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Subset of ( ( ) ( ) set ) ) ) ,a : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) ) & ( b : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) <_ o9 : ( ( ) ( Relation-like ) Element of LinOrders b₁ : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Subset of ( ( ) ( ) set ) ) ) ,a : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) implies b : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) <_ o : ( ( ) ( Relation-like ) Element of LinOrders b₁ : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Subset of ( ( ) ( ) set ) ) ) ,a : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) ) ) ) ) ;

theorem :: ARROW:13

for A being ( ( non empty ) ( non empty ) set )
for o being ( ( ) ( Relation-like ) Element of LinOrders A : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Subset of ( ( ) ( ) set ) ) )
for o9 being ( ( ) ( Relation-like ) Element of LinPreorders A : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) holds
( ( for a, b being ( ( ) ( ) Element of A : ( ( non empty ) ( non empty ) set ) ) st a : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) <_ o : ( ( ) ( Relation-like ) Element of LinOrders b₁ : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Subset of ( ( ) ( ) set ) ) ) ,b : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) holds
a : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) <_ o9 : ( ( ) ( Relation-like ) Element of LinPreorders b₁ : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) ) iff for a, b being ( ( ) ( ) Element of A : ( ( non empty ) ( non empty ) set ) ) holds
( a : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) <_ o : ( ( ) ( Relation-like ) Element of LinOrders b₁ : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Subset of ( ( ) ( ) set ) ) ) ,b : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) iff a : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) <_ o9 : ( ( ) ( Relation-like ) Element of LinPreorders b₁ : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of b₁ : ( ( non empty ) ( non empty ) set ) ) ) ) ;

theorem :: ARROW:14

for A, N being ( ( non empty finite ) ( non empty finite ) set )
for f being ( ( Function-like quasi_total ) ( Relation-like Funcs (b₂ : ( ( non empty finite ) ( non empty finite ) set ) ,(LinPreorders b₁ : ( ( non empty finite ) ( non empty finite ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b₂ : ( ( non empty finite ) ( non empty finite ) set ) , LinPreorders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) set ) ) -defined LinPreorders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of Funcs (N : ( ( non empty finite ) ( non empty finite ) set ) ,(LinPreorders A : ( ( non empty finite ) ( non empty finite ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b₂ : ( ( non empty finite ) ( non empty finite ) set ) , LinPreorders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) set ) ) , LinPreorders A : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) set ) ) st ( for p being ( ( ) ( Relation-like b₂ : ( ( non empty finite ) ( non empty finite ) set ) -defined LinPreorders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Element of Funcs (N : ( ( non empty finite ) ( non empty finite ) set ) ,(LinPreorders A : ( ( non empty finite ) ( non empty finite ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b₂ : ( ( non empty finite ) ( non empty finite ) set ) , LinPreorders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) set ) ) )
for a, b being ( ( ) ( ) Element of A : ( ( non empty finite ) ( non empty finite ) set ) ) st ( for i being ( ( ) ( ) Element of N : ( ( non empty finite ) ( non empty finite ) set ) ) holds a : ( ( ) ( Relation-like b₂ : ( ( non empty finite ) ( non empty finite ) set ) -defined LinPreorders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Element of Funcs (b₂ : ( ( non empty finite ) ( non empty finite ) set ) ,(LinPreorders b₁ : ( ( non empty finite ) ( non empty finite ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b₂ : ( ( non empty finite ) ( non empty finite ) set ) , LinPreorders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) set ) ) ) <_ p : ( ( ) ( ) Element of b₂ : ( ( non empty finite ) ( non empty finite ) set ) ) . i : ( ( ) ( ) Element of b₁ : ( ( non empty finite ) ( non empty finite ) set ) ) : ( ( ) ( Relation-like ) Element of LinPreorders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of b₁ : ( ( non empty finite ) ( non empty finite ) set ) ) ) holds
a : ( ( ) ( Relation-like b₂ : ( ( non empty finite ) ( non empty finite ) set ) -defined LinPreorders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Element of Funcs (b₂ : ( ( non empty finite ) ( non empty finite ) set ) ,(LinPreorders b₁ : ( ( non empty finite ) ( non empty finite ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b₂ : ( ( non empty finite ) ( non empty finite ) set ) , LinPreorders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) set ) ) ) <_ f : ( ( Function-like quasi_total ) ( Relation-like Funcs (b₂ : ( ( non empty finite ) ( non empty finite ) set ) ,(LinPreorders b₁ : ( ( non empty finite ) ( non empty finite ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b₂ : ( ( non empty finite ) ( non empty finite ) set ) , LinPreorders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) set ) ) -defined LinPreorders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of Funcs (b₂ : ( ( non empty finite ) ( non empty finite ) set ) ,(LinPreorders b₁ : ( ( non empty finite ) ( non empty finite ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b₂ : ( ( non empty finite ) ( non empty finite ) set ) , LinPreorders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) set ) ) , LinPreorders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) set ) ) . p : ( ( ) ( ) Element of b₂ : ( ( non empty finite ) ( non empty finite ) set ) ) : ( ( ) ( Relation-like ) Element of LinPreorders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of b₁ : ( ( non empty finite ) ( non empty finite ) set ) ) ) & ( for p, p9 being ( ( ) ( Relation-like b₂ : ( ( non empty finite ) ( non empty finite ) set ) -defined LinPreorders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Element of Funcs (N : ( ( non empty finite ) ( non empty finite ) set ) ,(LinPreorders A : ( ( non empty finite ) ( non empty finite ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b₂ : ( ( non empty finite ) ( non empty finite ) set ) , LinPreorders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) set ) ) )
for a, b being ( ( ) ( ) Element of A : ( ( non empty finite ) ( non empty finite ) set ) ) st ( for i being ( ( ) ( ) Element of N : ( ( non empty finite ) ( non empty finite ) set ) ) holds
( ( a : ( ( ) ( ) Element of b₁ : ( ( non empty finite ) ( non empty finite ) set ) ) <_ p : ( ( ) ( ) Element of b₂ : ( ( non empty finite ) ( non empty finite ) set ) ) . i : ( ( ) ( ) Element of b₂ : ( ( non empty finite ) ( non empty finite ) set ) ) : ( ( ) ( Relation-like ) Element of LinPreorders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of b₁ : ( ( non empty finite ) ( non empty finite ) set ) ) implies a : ( ( ) ( ) Element of b₁ : ( ( non empty finite ) ( non empty finite ) set ) ) <_ p9 : ( ( ) ( Relation-like b₂ : ( ( non empty finite ) ( non empty finite ) set ) -defined LinPreorders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Element of Funcs (b₂ : ( ( non empty finite ) ( non empty finite ) set ) ,(LinPreorders b₁ : ( ( non empty finite ) ( non empty finite ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b₂ : ( ( non empty finite ) ( non empty finite ) set ) , LinPreorders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) set ) ) ) . i : ( ( ) ( ) Element of b₂ : ( ( non empty finite ) ( non empty finite ) set ) ) : ( ( ) ( Relation-like ) Element of LinPreorders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of b₁ : ( ( non empty finite ) ( non empty finite ) set ) ) ) & ( a : ( ( ) ( ) Element of b₁ : ( ( non empty finite ) ( non empty finite ) set ) ) <_ p9 : ( ( ) ( Relation-like b₂ : ( ( non empty finite ) ( non empty finite ) set ) -defined LinPreorders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Element of Funcs (b₂ : ( ( non empty finite ) ( non empty finite ) set ) ,(LinPreorders b₁ : ( ( non empty finite ) ( non empty finite ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b₂ : ( ( non empty finite ) ( non empty finite ) set ) , LinPreorders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) set ) ) ) . i : ( ( ) ( ) Element of b₂ : ( ( non empty finite ) ( non empty finite ) set ) ) : ( ( ) ( Relation-like ) Element of LinPreorders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of b₁ : ( ( non empty finite ) ( non empty finite ) set ) ) implies a : ( ( ) ( ) Element of b₁ : ( ( non empty finite ) ( non empty finite ) set ) ) <_ p : ( ( ) ( ) Element of b₂ : ( ( non empty finite ) ( non empty finite ) set ) ) . i : ( ( ) ( ) Element of b₂ : ( ( non empty finite ) ( non empty finite ) set ) ) : ( ( ) ( Relation-like ) Element of LinPreorders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of b₁ : ( ( non empty finite ) ( non empty finite ) set ) ) ) & ( b : ( ( ) ( ) Element of b₁ : ( ( non empty finite ) ( non empty finite ) set ) ) <_ p : ( ( ) ( ) Element of b₂ : ( ( non empty finite ) ( non empty finite ) set ) ) . i : ( ( ) ( ) Element of b₂ : ( ( non empty finite ) ( non empty finite ) set ) ) : ( ( ) ( Relation-like ) Element of LinPreorders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) set ) ) ,a : ( ( ) ( ) Element of b₁ : ( ( non empty finite ) ( non empty finite ) set ) ) implies b : ( ( ) ( ) Element of b₁ : ( ( non empty finite ) ( non empty finite ) set ) ) <_ p9 : ( ( ) ( Relation-like b₂ : ( ( non empty finite ) ( non empty finite ) set ) -defined LinPreorders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Element of Funcs (b₂ : ( ( non empty finite ) ( non empty finite ) set ) ,(LinPreorders b₁ : ( ( non empty finite ) ( non empty finite ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b₂ : ( ( non empty finite ) ( non empty finite ) set ) , LinPreorders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) set ) ) ) . i : ( ( ) ( ) Element of b₂ : ( ( non empty finite ) ( non empty finite ) set ) ) : ( ( ) ( Relation-like ) Element of LinPreorders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) set ) ) ,a : ( ( ) ( ) Element of b₁ : ( ( non empty finite ) ( non empty finite ) set ) ) ) & ( b : ( ( ) ( ) Element of b₁ : ( ( non empty finite ) ( non empty finite ) set ) ) <_ p9 : ( ( ) ( Relation-like b₂ : ( ( non empty finite ) ( non empty finite ) set ) -defined LinPreorders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Element of Funcs (b₂ : ( ( non empty finite ) ( non empty finite ) set ) ,(LinPreorders b₁ : ( ( non empty finite ) ( non empty finite ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b₂ : ( ( non empty finite ) ( non empty finite ) set ) , LinPreorders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) set ) ) ) . i : ( ( ) ( ) Element of b₂ : ( ( non empty finite ) ( non empty finite ) set ) ) : ( ( ) ( Relation-like ) Element of LinPreorders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) set ) ) ,a : ( ( ) ( ) Element of b₁ : ( ( non empty finite ) ( non empty finite ) set ) ) implies b : ( ( ) ( ) Element of b₁ : ( ( non empty finite ) ( non empty finite ) set ) ) <_ p : ( ( ) ( ) Element of b₂ : ( ( non empty finite ) ( non empty finite ) set ) ) . i : ( ( ) ( ) Element of b₂ : ( ( non empty finite ) ( non empty finite ) set ) ) : ( ( ) ( Relation-like ) Element of LinPreorders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) set ) ) ,a : ( ( ) ( ) Element of b₁ : ( ( non empty finite ) ( non empty finite ) set ) ) ) ) ) holds
( a : ( ( ) ( ) Element of b₁ : ( ( non empty finite ) ( non empty finite ) set ) ) <_ f : ( ( Function-like quasi_total ) ( Relation-like Funcs (b₂ : ( ( non empty finite ) ( non empty finite ) set ) ,(LinPreorders b₁ : ( ( non empty finite ) ( non empty finite ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b₂ : ( ( non empty finite ) ( non empty finite ) set ) , LinPreorders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) set ) ) -defined LinPreorders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of Funcs (b₂ : ( ( non empty finite ) ( non empty finite ) set ) ,(LinPreorders b₁ : ( ( non empty finite ) ( non empty finite ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b₂ : ( ( non empty finite ) ( non empty finite ) set ) , LinPreorders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) set ) ) , LinPreorders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) set ) ) . p : ( ( ) ( ) Element of b₂ : ( ( non empty finite ) ( non empty finite ) set ) ) : ( ( ) ( Relation-like ) Element of LinPreorders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of b₁ : ( ( non empty finite ) ( non empty finite ) set ) ) iff a : ( ( ) ( ) Element of b₁ : ( ( non empty finite ) ( non empty finite ) set ) ) <_ f : ( ( Function-like quasi_total ) ( Relation-like Funcs (b₂ : ( ( non empty finite ) ( non empty finite ) set ) ,(LinPreorders b₁ : ( ( non empty finite ) ( non empty finite ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b₂ : ( ( non empty finite ) ( non empty finite ) set ) , LinPreorders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) set ) ) -defined LinPreorders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of Funcs (b₂ : ( ( non empty finite ) ( non empty finite ) set ) ,(LinPreorders b₁ : ( ( non empty finite ) ( non empty finite ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b₂ : ( ( non empty finite ) ( non empty finite ) set ) , LinPreorders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) set ) ) , LinPreorders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) set ) ) . p9 : ( ( ) ( Relation-like b₂ : ( ( non empty finite ) ( non empty finite ) set ) -defined LinPreorders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Element of Funcs (b₂ : ( ( non empty finite ) ( non empty finite ) set ) ,(LinPreorders b₁ : ( ( non empty finite ) ( non empty finite ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b₂ : ( ( non empty finite ) ( non empty finite ) set ) , LinPreorders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like ) Element of LinPreorders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of b₁ : ( ( non empty finite ) ( non empty finite ) set ) ) ) ) & card A : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( ext-real non negative V24() V25() V26() V30() V31() V32() V44() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) set ) ) >= 3 : ( ( ) ( ext-real positive non negative non empty V24() V25() V26() V30() V31() V32() V44() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) holds
ex n being ( ( ) ( ) Element of N : ( ( non empty finite ) ( non empty finite ) set ) ) st
for p being ( ( ) ( Relation-like b₂ : ( ( non empty finite ) ( non empty finite ) set ) -defined LinPreorders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Element of Funcs (N : ( ( non empty finite ) ( non empty finite ) set ) ,(LinPreorders A : ( ( non empty finite ) ( non empty finite ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b₂ : ( ( non empty finite ) ( non empty finite ) set ) , LinPreorders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) set ) ) )
for a, b being ( ( ) ( ) Element of A : ( ( non empty finite ) ( non empty finite ) set ) ) st a : ( ( ) ( ) Element of b₁ : ( ( non empty finite ) ( non empty finite ) set ) ) <_ p : ( ( ) ( Relation-like b₂ : ( ( non empty finite ) ( non empty finite ) set ) -defined LinPreorders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Element of Funcs (b₂ : ( ( non empty finite ) ( non empty finite ) set ) ,(LinPreorders b₁ : ( ( non empty finite ) ( non empty finite ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b₂ : ( ( non empty finite ) ( non empty finite ) set ) , LinPreorders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) set ) ) ) . n : ( ( ) ( ) Element of b₂ : ( ( non empty finite ) ( non empty finite ) set ) ) : ( ( ) ( Relation-like ) Element of LinPreorders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of b₁ : ( ( non empty finite ) ( non empty finite ) set ) ) holds
a : ( ( ) ( ) Element of b₁ : ( ( non empty finite ) ( non empty finite ) set ) ) <_ f : ( ( Function-like quasi_total ) ( Relation-like Funcs (b₂ : ( ( non empty finite ) ( non empty finite ) set ) ,(LinPreorders b₁ : ( ( non empty finite ) ( non empty finite ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b₂ : ( ( non empty finite ) ( non empty finite ) set ) , LinPreorders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) set ) ) -defined LinPreorders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of Funcs (b₂ : ( ( non empty finite ) ( non empty finite ) set ) ,(LinPreorders b₁ : ( ( non empty finite ) ( non empty finite ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b₂ : ( ( non empty finite ) ( non empty finite ) set ) , LinPreorders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) set ) ) , LinPreorders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) set ) ) . p : ( ( ) ( Relation-like b₂ : ( ( non empty finite ) ( non empty finite ) set ) -defined LinPreorders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Element of Funcs (b₂ : ( ( non empty finite ) ( non empty finite ) set ) ,(LinPreorders b₁ : ( ( non empty finite ) ( non empty finite ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b₂ : ( ( non empty finite ) ( non empty finite ) set ) , LinPreorders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like ) Element of LinPreorders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of b₁ : ( ( non empty finite ) ( non empty finite ) set ) ) ;

theorem :: ARROW:15

for A, N being ( ( non empty finite ) ( non empty finite ) set )
for f being ( ( Function-like quasi_total ) ( Relation-like Funcs (b₂ : ( ( non empty finite ) ( non empty finite ) set ) ,(LinOrders b₁ : ( ( non empty finite ) ( non empty finite ) set ) ) : ( ( ) ( non empty ) Subset of ( ( ) ( ) set ) ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b₂ : ( ( non empty finite ) ( non empty finite ) set ) , LinOrders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) Subset of ( ( ) ( ) set ) ) ) -defined LinPreorders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of Funcs (N : ( ( non empty finite ) ( non empty finite ) set ) ,(LinOrders A : ( ( non empty finite ) ( non empty finite ) set ) ) : ( ( ) ( non empty ) Subset of ( ( ) ( ) set ) ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b₂ : ( ( non empty finite ) ( non empty finite ) set ) , LinOrders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) Subset of ( ( ) ( ) set ) ) ) , LinPreorders A : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) set ) ) st ( for p being ( ( ) ( Relation-like b₂ : ( ( non empty finite ) ( non empty finite ) set ) -defined LinOrders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) Subset of ( ( ) ( ) set ) ) -valued Function-like quasi_total ) Element of Funcs (N : ( ( non empty finite ) ( non empty finite ) set ) ,(LinOrders A : ( ( non empty finite ) ( non empty finite ) set ) ) : ( ( ) ( non empty ) Subset of ( ( ) ( ) set ) ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b₂ : ( ( non empty finite ) ( non empty finite ) set ) , LinOrders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) Subset of ( ( ) ( ) set ) ) ) )
for a, b being ( ( ) ( ) Element of A : ( ( non empty finite ) ( non empty finite ) set ) ) st ( for i being ( ( ) ( ) Element of N : ( ( non empty finite ) ( non empty finite ) set ) ) holds a : ( ( ) ( Relation-like b₂ : ( ( non empty finite ) ( non empty finite ) set ) -defined LinOrders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) Subset of ( ( ) ( ) set ) ) -valued Function-like quasi_total ) Element of Funcs (b₂ : ( ( non empty finite ) ( non empty finite ) set ) ,(LinOrders b₁ : ( ( non empty finite ) ( non empty finite ) set ) ) : ( ( ) ( non empty ) Subset of ( ( ) ( ) set ) ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b₂ : ( ( non empty finite ) ( non empty finite ) set ) , LinOrders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) Subset of ( ( ) ( ) set ) ) ) ) <_ p : ( ( ) ( ) Element of b₂ : ( ( non empty finite ) ( non empty finite ) set ) ) . i : ( ( ) ( ) Element of b₁ : ( ( non empty finite ) ( non empty finite ) set ) ) : ( ( ) ( Relation-like ) Element of LinOrders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) Subset of ( ( ) ( ) set ) ) ) ,b : ( ( ) ( ) Element of b₁ : ( ( non empty finite ) ( non empty finite ) set ) ) ) holds
a : ( ( ) ( Relation-like b₂ : ( ( non empty finite ) ( non empty finite ) set ) -defined LinOrders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) Subset of ( ( ) ( ) set ) ) -valued Function-like quasi_total ) Element of Funcs (b₂ : ( ( non empty finite ) ( non empty finite ) set ) ,(LinOrders b₁ : ( ( non empty finite ) ( non empty finite ) set ) ) : ( ( ) ( non empty ) Subset of ( ( ) ( ) set ) ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b₂ : ( ( non empty finite ) ( non empty finite ) set ) , LinOrders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) Subset of ( ( ) ( ) set ) ) ) ) <_ f : ( ( Function-like quasi_total ) ( Relation-like Funcs (b₂ : ( ( non empty finite ) ( non empty finite ) set ) ,(LinOrders b₁ : ( ( non empty finite ) ( non empty finite ) set ) ) : ( ( ) ( non empty ) Subset of ( ( ) ( ) set ) ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b₂ : ( ( non empty finite ) ( non empty finite ) set ) , LinOrders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) Subset of ( ( ) ( ) set ) ) ) -defined LinPreorders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of Funcs (b₂ : ( ( non empty finite ) ( non empty finite ) set ) ,(LinOrders b₁ : ( ( non empty finite ) ( non empty finite ) set ) ) : ( ( ) ( non empty ) Subset of ( ( ) ( ) set ) ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b₂ : ( ( non empty finite ) ( non empty finite ) set ) , LinOrders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) Subset of ( ( ) ( ) set ) ) ) , LinPreorders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) set ) ) . p : ( ( ) ( ) Element of b₂ : ( ( non empty finite ) ( non empty finite ) set ) ) : ( ( ) ( Relation-like ) Element of LinPreorders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of b₁ : ( ( non empty finite ) ( non empty finite ) set ) ) ) & ( for p, p9 being ( ( ) ( Relation-like b₂ : ( ( non empty finite ) ( non empty finite ) set ) -defined LinOrders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) Subset of ( ( ) ( ) set ) ) -valued Function-like quasi_total ) Element of Funcs (N : ( ( non empty finite ) ( non empty finite ) set ) ,(LinOrders A : ( ( non empty finite ) ( non empty finite ) set ) ) : ( ( ) ( non empty ) Subset of ( ( ) ( ) set ) ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b₂ : ( ( non empty finite ) ( non empty finite ) set ) , LinOrders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) Subset of ( ( ) ( ) set ) ) ) )
for a, b being ( ( ) ( ) Element of A : ( ( non empty finite ) ( non empty finite ) set ) ) st ( for i being ( ( ) ( ) Element of N : ( ( non empty finite ) ( non empty finite ) set ) ) holds
( a : ( ( ) ( ) Element of b₁ : ( ( non empty finite ) ( non empty finite ) set ) ) <_ p : ( ( ) ( ) Element of b₂ : ( ( non empty finite ) ( non empty finite ) set ) ) . i : ( ( ) ( ) Element of b₂ : ( ( non empty finite ) ( non empty finite ) set ) ) : ( ( ) ( Relation-like ) Element of LinOrders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) Subset of ( ( ) ( ) set ) ) ) ,b : ( ( ) ( ) Element of b₁ : ( ( non empty finite ) ( non empty finite ) set ) ) iff a : ( ( ) ( ) Element of b₁ : ( ( non empty finite ) ( non empty finite ) set ) ) <_ p9 : ( ( ) ( Relation-like b₂ : ( ( non empty finite ) ( non empty finite ) set ) -defined LinOrders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) Subset of ( ( ) ( ) set ) ) -valued Function-like quasi_total ) Element of Funcs (b₂ : ( ( non empty finite ) ( non empty finite ) set ) ,(LinOrders b₁ : ( ( non empty finite ) ( non empty finite ) set ) ) : ( ( ) ( non empty ) Subset of ( ( ) ( ) set ) ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b₂ : ( ( non empty finite ) ( non empty finite ) set ) , LinOrders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) Subset of ( ( ) ( ) set ) ) ) ) . i : ( ( ) ( ) Element of b₂ : ( ( non empty finite ) ( non empty finite ) set ) ) : ( ( ) ( Relation-like ) Element of LinOrders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) Subset of ( ( ) ( ) set ) ) ) ,b : ( ( ) ( ) Element of b₁ : ( ( non empty finite ) ( non empty finite ) set ) ) ) ) holds
( a : ( ( ) ( ) Element of b₁ : ( ( non empty finite ) ( non empty finite ) set ) ) <_ f : ( ( Function-like quasi_total ) ( Relation-like Funcs (b₂ : ( ( non empty finite ) ( non empty finite ) set ) ,(LinOrders b₁ : ( ( non empty finite ) ( non empty finite ) set ) ) : ( ( ) ( non empty ) Subset of ( ( ) ( ) set ) ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b₂ : ( ( non empty finite ) ( non empty finite ) set ) , LinOrders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) Subset of ( ( ) ( ) set ) ) ) -defined LinPreorders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of Funcs (b₂ : ( ( non empty finite ) ( non empty finite ) set ) ,(LinOrders b₁ : ( ( non empty finite ) ( non empty finite ) set ) ) : ( ( ) ( non empty ) Subset of ( ( ) ( ) set ) ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b₂ : ( ( non empty finite ) ( non empty finite ) set ) , LinOrders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) Subset of ( ( ) ( ) set ) ) ) , LinPreorders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) set ) ) . p : ( ( ) ( ) Element of b₂ : ( ( non empty finite ) ( non empty finite ) set ) ) : ( ( ) ( Relation-like ) Element of LinPreorders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of b₁ : ( ( non empty finite ) ( non empty finite ) set ) ) iff a : ( ( ) ( ) Element of b₁ : ( ( non empty finite ) ( non empty finite ) set ) ) <_ f : ( ( Function-like quasi_total ) ( Relation-like Funcs (b₂ : ( ( non empty finite ) ( non empty finite ) set ) ,(LinOrders b₁ : ( ( non empty finite ) ( non empty finite ) set ) ) : ( ( ) ( non empty ) Subset of ( ( ) ( ) set ) ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b₂ : ( ( non empty finite ) ( non empty finite ) set ) , LinOrders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) Subset of ( ( ) ( ) set ) ) ) -defined LinPreorders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of Funcs (b₂ : ( ( non empty finite ) ( non empty finite ) set ) ,(LinOrders b₁ : ( ( non empty finite ) ( non empty finite ) set ) ) : ( ( ) ( non empty ) Subset of ( ( ) ( ) set ) ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b₂ : ( ( non empty finite ) ( non empty finite ) set ) , LinOrders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) Subset of ( ( ) ( ) set ) ) ) , LinPreorders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) set ) ) . p9 : ( ( ) ( Relation-like b₂ : ( ( non empty finite ) ( non empty finite ) set ) -defined LinOrders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) Subset of ( ( ) ( ) set ) ) -valued Function-like quasi_total ) Element of Funcs (b₂ : ( ( non empty finite ) ( non empty finite ) set ) ,(LinOrders b₁ : ( ( non empty finite ) ( non empty finite ) set ) ) : ( ( ) ( non empty ) Subset of ( ( ) ( ) set ) ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b₂ : ( ( non empty finite ) ( non empty finite ) set ) , LinOrders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) Subset of ( ( ) ( ) set ) ) ) ) : ( ( ) ( Relation-like ) Element of LinPreorders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of b₁ : ( ( non empty finite ) ( non empty finite ) set ) ) ) ) & card A : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( ext-real non negative V24() V25() V26() V30() V31() V32() V44() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) set ) ) >= 3 : ( ( ) ( ext-real positive non negative non empty V24() V25() V26() V30() V31() V32() V44() ) Element of NAT : ( ( ) ( non empty V24() V25() V26() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) holds
ex n being ( ( ) ( ) Element of N : ( ( non empty finite ) ( non empty finite ) set ) ) st
for p being ( ( ) ( Relation-like b₂ : ( ( non empty finite ) ( non empty finite ) set ) -defined LinOrders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) Subset of ( ( ) ( ) set ) ) -valued Function-like quasi_total ) Element of Funcs (N : ( ( non empty finite ) ( non empty finite ) set ) ,(LinOrders A : ( ( non empty finite ) ( non empty finite ) set ) ) : ( ( ) ( non empty ) Subset of ( ( ) ( ) set ) ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b₂ : ( ( non empty finite ) ( non empty finite ) set ) , LinOrders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) Subset of ( ( ) ( ) set ) ) ) )
for a, b being ( ( ) ( ) Element of A : ( ( non empty finite ) ( non empty finite ) set ) ) holds
( a : ( ( ) ( ) Element of b₁ : ( ( non empty finite ) ( non empty finite ) set ) ) <_ p : ( ( ) ( Relation-like b₂ : ( ( non empty finite ) ( non empty finite ) set ) -defined LinOrders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) Subset of ( ( ) ( ) set ) ) -valued Function-like quasi_total ) Element of Funcs (b₂ : ( ( non empty finite ) ( non empty finite ) set ) ,(LinOrders b₁ : ( ( non empty finite ) ( non empty finite ) set ) ) : ( ( ) ( non empty ) Subset of ( ( ) ( ) set ) ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b₂ : ( ( non empty finite ) ( non empty finite ) set ) , LinOrders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) Subset of ( ( ) ( ) set ) ) ) ) . n : ( ( ) ( ) Element of b₂ : ( ( non empty finite ) ( non empty finite ) set ) ) : ( ( ) ( Relation-like ) Element of LinOrders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) Subset of ( ( ) ( ) set ) ) ) ,b : ( ( ) ( ) Element of b₁ : ( ( non empty finite ) ( non empty finite ) set ) ) iff a : ( ( ) ( ) Element of b₁ : ( ( non empty finite ) ( non empty finite ) set ) ) <_ f : ( ( Function-like quasi_total ) ( Relation-like Funcs (b₂ : ( ( non empty finite ) ( non empty finite ) set ) ,(LinOrders b₁ : ( ( non empty finite ) ( non empty finite ) set ) ) : ( ( ) ( non empty ) Subset of ( ( ) ( ) set ) ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b₂ : ( ( non empty finite ) ( non empty finite ) set ) , LinOrders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) Subset of ( ( ) ( ) set ) ) ) -defined LinPreorders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of Funcs (b₂ : ( ( non empty finite ) ( non empty finite ) set ) ,(LinOrders b₁ : ( ( non empty finite ) ( non empty finite ) set ) ) : ( ( ) ( non empty ) Subset of ( ( ) ( ) set ) ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b₂ : ( ( non empty finite ) ( non empty finite ) set ) , LinOrders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) Subset of ( ( ) ( ) set ) ) ) , LinPreorders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) set ) ) . p : ( ( ) ( Relation-like b₂ : ( ( non empty finite ) ( non empty finite ) set ) -defined LinOrders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) Subset of ( ( ) ( ) set ) ) -valued Function-like quasi_total ) Element of Funcs (b₂ : ( ( non empty finite ) ( non empty finite ) set ) ,(LinOrders b₁ : ( ( non empty finite ) ( non empty finite ) set ) ) : ( ( ) ( non empty ) Subset of ( ( ) ( ) set ) ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of b₂ : ( ( non empty finite ) ( non empty finite ) set ) , LinOrders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) Subset of ( ( ) ( ) set ) ) ) ) : ( ( ) ( Relation-like ) Element of LinPreorders b₁ : ( ( non empty finite ) ( non empty finite ) set ) : ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of b₁ : ( ( non empty finite ) ( non empty finite ) set ) ) ) ;