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;