theorem Th33: :: CARDFIL4:41

ex cB being basis of (Frechet_Filter NAT) st
( cB = base_of_frechet_filter & [:cB,cB:] is basis of <.(Frechet_Filter NAT),(Frechet_Filter NAT).) )