let n be Nat; :: thesis: for X being set

for Fx being Subset-Family of X st order Fx <= n holds

Fx is finite-order

let X be set ; :: thesis: for Fx being Subset-Family of X st order Fx <= n holds

Fx is finite-order

let Fx be Subset-Family of X; :: thesis: ( order Fx <= n implies Fx is finite-order )

assume order Fx <= n ; :: thesis: Fx is finite-order

then order Fx <> +infty by XXREAL_0:4;

hence Fx is finite-order by Def2; :: thesis: verum

for Fx being Subset-Family of X st order Fx <= n holds

Fx is finite-order

let X be set ; :: thesis: for Fx being Subset-Family of X st order Fx <= n holds

Fx is finite-order

let Fx be Subset-Family of X; :: thesis: ( order Fx <= n implies Fx is finite-order )

assume order Fx <= n ; :: thesis: Fx is finite-order

then order Fx <> +infty by XXREAL_0:4;

hence Fx is finite-order by Def2; :: thesis: verum