set O = T;
set a = HC (p,T);

now

assume HC (p,T) = 0. L ; :: thesis: contradiction
then not HT (p,T) in Support p by POLYNOM1:def 9;
then Support p = {} by Def6;
then p = 0_ (n,L) by POLYNOM7:1;
hence contradiction by POLYNOM7:def 2; :: thesis: verum

end;

hence not HC (p,T) is zero by STRUCT_0:def 12; :: thesis: verum