Proposes a linear sequent calculus for subtyping in programming languages as logical entailment, allowing the derivation of a complete and coherent approach to subtyping from logically meaningful sequents. Entailment in the frame of a second-order sequent calculus; Cut-elimination theorem equivalent; Derivation of transitivity and anti-symmetry from elementary logical principles.