Abstract: In 1, a type system λω× ≤ is proposed and studied, which is obtained by extending the type system λω × in 2 with subtyping and bounded quantification. λω× ≤ differs from those extensions of system F in distinguishing operator context, and subtyping context from term context. In this paper, the PER model of λω× ≤ is studied as its semantic model and the soundness of the PER model is discussed.