:: deftheorem defines 2-CRoot(2) FIELD_10:def 7 :
2-CRoot(2) = sqrt 2;