:: deftheorem Def2 defines order TOPDIM_2:def 2 :
for X being set
for Fx being Subset-Family of X
for b₃ being ExtReal holds
( ( Fx is finite-order implies ( b₃ = order Fx iff ( ( for Gx being Subset-Family of X st b₃ + 1 in card Gx & Gx c= Fx holds
meet Gx is empty ) & ex Gx being Subset-Family of X st
( Gx c= Fx & card Gx = b₃ + 1 & ( not meet Gx is empty or Gx is empty ) ) ) ) ) & ( not Fx is finite-order implies ( b₃ = order Fx iff b₃ = +infty ) ) );