theorem Th9: :: CARDFIL4:9

{ [0,n] where n is Nat : verum } is infinite