scheme :: ASYMPT_0:sch 1
FinSegRng1{ F₁() -> Nat, F₂() -> Nat, F₃() -> non empty set , F₄( set ) -> Element of F₃() } :

{ F₄(i) where i is Element of NAT : ( F₁() <= i & i <= F₂() ) } is non empty finite Subset of F₃()

provided

A1: F₁() <= F₂()