theorem :: FIELD_10:16

3-Root(2) |^ 3 = 2 by R32;