theorem HcfLat: :: MOEBIUS2:61

hcflatplus = hcflat || NATPLUS