theorem Th36: :: CARDFIL4:44

<.all-square-uparrow.) = <.(Frechet_Filter NAT),(Frechet_Filter NAT).) by Th34, CARDFIL2:19, Th35;