now :: thesis: ( not deg (E,F) = - 1 implies deg (E,F) is natural )

assume A1: not deg (E,F) = - 1 ; :: thesis: deg (E,F) is natural
dim (VecSp (E,F)) is Nat ;
hence deg (E,F) is natural by Def6, A1; :: thesis: verum

end;

hence deg (E,F) is dim-like ; :: thesis: verum