for A, N being non empty finite set
for f being Function of (Funcs (N,(LinOrders A))),(LinPreorders A) st ( for p being Element of Funcs (N,(LinOrders A))
for a, b being Element of A st ( for i being Element of N holds a <_ p . i,b ) holds
a <_ f . p,b ) & ( for p, p9 being Element of Funcs (N,(LinOrders A))
for a, b being Element of A st ( for i being Element of N holds
( a <_ p . i,b iff a <_ p9 . i,b ) ) holds
( a <_ f . p,b iff a <_ f . p9,b ) ) & card A >= 3 holds
ex n being Element of N st
for p being Element of Funcs (N,(LinOrders A))
for a, b being Element of A holds
( a <_ p . n,b iff a <_ f . p,b )