theorem Th38: :: CARDFIL4:46

( [:NAT,NAT:] \ { [0,n] where n is Nat : verum } in <.(Frechet_Filter NAT),(Frechet_Filter NAT).) & not [:NAT,NAT:] \ { [0,n] where n is Nat : verum } in Frechet_Filter [:NAT,NAT:] )