theorem Th2: :: LTLAXIO3:2

NAT --> {} is LTLModel