theorem Lm17: :: HILBERT4:10

{} tohilb = (0,1) --> (1,0)