x <> 0. F ;
hence (x ") " = x by Th20; :: thesis: verum