let L be non empty ZeroStr ; :: thesis: for p being Polynomial of L holds deg p >= - 1
let p be Polynomial of L; :: thesis: deg p >= - 1
per cases ( p = 0_. L or p <> 0_. L ) ;
suppose p = 0_. L ; :: thesis: deg p >= - 1
hence deg p >= - 1 by Th20; :: thesis: verum
end;
suppose p <> 0_. L ; :: thesis: deg p >= - 1
hence deg p >= - 1 by Lm8; :: thesis: verum
end;
end;