theorem Lm18: :: HILBERT4:9

for x being set st x <> {} holds
x tohilb = id 1