Summary: Over the last several years there has been growing interest in object- oriented languages in the programming languages community, and this interest has spread to other technical communities such as those in software engineering and data base. (Note. In this paper we consider object-oriented languages to be those which include support for inheritance on subtypes.) Simula 67 and Smalltalk in their various incarnations represent the earliest work on object-oriented languages. More recently other languages have been developed including C++ and VBase (both based on C), Flavors and LOOPS (extensions of LISP), OWL (based on Clu), and Eiffel. {\it L. Cardelli} [ibid. 76, 138-164 (1988)] (an earlier version of which appeared in 1984) developed one of the earliest formal approaches to inheritance, introducing both the syntax and semantics of an extension of the classical typed lambda calculus supporting inheritance. Building on some earlier work on type containment by {\it J. C. Mitchell} [Inform. and Comput. 76, 211-249 (1988)], {\it L. Cardelli} and {\it P. Wegner} [(*) ACM Comput. Surveys 17, 47-522 (1985)] presented an extension of the second-order lambda calculus supporting inheritance. This language supported both parametric and subtype (inheritance) polymorphism by means of bounded quantification. We use the notation introduced in (*) including their name for the language, Bounded Fun. This paper originated in an attempt to formulate a sound model for Bounded Fun.