theorem Th16: :: ABCMIZ_1:16

{ [{},i] where i is Element of NAT : verum } c= Vars