theorem Th35: :: CARDFIL4:43

<.[:base_of_frechet_filter,base_of_frechet_filter:].) = <.(Frechet_Filter NAT),(Frechet_Filter NAT).)