theorem Th125: :: HILB10_7:125

for n, k, m being Nat st k <= n holds
doms (k,m) c= doms (n,m)