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