Loading [MathJax]/extensions/tex2jax.js
Lm1:
for X being set holds
( X is countable iff ex f being Function st
( dom f = RAT & X c= rng f ) )
by CARD_1:12, TOPGEN_3:17;
Lm2:
for T being set
for F being Subset-Family of T st F is SigmaField of T holds
F is closed_for_countable_unions