for N being finite Subset of NAT ex Order being Function of N,(Segm (card N)) st
( Order is bijective & ( for n, k being Nat st n in dom Order & k in dom Order & n < k holds
Order . n < Order . k ) )