circle (a,b,0) = {|[a,b]|} by Thm23;
hence circle (a,b,0) is trivial ; :: thesis: verum