The minimal-coset projection onto W^I is order-preserving, and Bruhat order on the parabolic quotient W^I

For the minimality clause of (1), write $w=P^I(w)v$ with $v\in W_I$ and $\mathrm{\ell }(w)=\mathrm{\ell }(P^I(w))+\mathrm{\ell }(v)$ by [F1], and fix a reduced expression $v=s_{i_1}\cdots s_{i_j}$ of $v$ (its letters lie in $I$). Then $P^I(w)=w_0\to w_1\to \cdots \to w_j=w$ with $w_l:=P^I(w)s_{i_1}\cdots s_{i_l}$, because $\mathrm{\ell }(w_l)=\mathrm{\ell }(P^I(w))+l$ by the additivity in [F1], so each step is right multiplication by a simple generator with strictly increasing length, hence a Bruhat edge; therefore $P^I(w)\le w$.

For the equality clause of (1): if $P^I(w)=w$ then $w\in W^I$ by definition of $P^I$; conversely, if $w\in W^I$, then $w$ lies in $W^I\cap w{W}_I$, whose unique element is $P^I(w)$ by [F1], so $P^I(w)=w$.

For the order-preservation in (1), prove $P^I(u)\le P^I(v)$ for all $u\le v$ by induction on $\mathrm{\ell }(v)$. Since $P^I(u)\le u\le v$ by step 1.1, the case $v\in W^I$ is immediate, because then $P^I(v)=v$ by step 1.2. If $v\mathrm{\notin }{W}^I$, then $D_R(v)\cap I\mathrm{\ne }\mathrm{\varnothing }$ by [F1], so there is $s\in I$ with $\mathrm{\ell }(vs)<\mathrm{\ell }(v)$; and $\mathrm{\ell }(P^I(u)s)>\mathrm{\ell }(P^I(u))$ because $P^I(u)\in W^I$. The lifting property [F4] applied to the pair $P^I(u)\le v$ gives $P^I(u)\le vs$. The induction hypothesis applies to the pair $(P^I(u),vs)$, whose second entry has smaller length, and yields $P^I(P^I(u))\le P^I(vs)$; here $P^I(P^I(u))=P^I(u)$ by step 1.2, and $P^I(vs)=P^I(v)$ because $vs$ and $v$ lie in the same left coset $v{W}_I$ and $P^I$ selects its minimal representative [F1]. Hence $P^I(u)\le P^I(v)$.

For (2), let $x\in W^I$, $y\in W$ with $x$ covered by $y$. If $y\mathrm{\notin }{W}^I$ then $y\mathrm{\ne }{P}^I(y)$ and $P^I(y)\le y$ with $P^I(y)<y$ by step 1.1; moreover $x=P^I(x)\le P^I(y)$ by step 2.1 applied to $x\le y$. Since $x$ is covered by $y$, the relation $x\le P^I(y)<y$ forces $P^I(y)=x$ (otherwise $x<P^I(y)<y$ would contradict the cover). The factorization $y=P^I(y)v$ with $v\in W_I$, $v\mathrm{\ne }1$ and $\mathrm{\ell }(y)=\mathrm{\ell }(P^I(y))+\mathrm{\ell }(v)$ then gives $\mathrm{\ell }(v)=\mathrm{\ell }(y)-\mathrm{\ell }(x)=1$ by [F8], so $v=s$ for an element $s\in I$ and $y=xs$.

For (4), let $u,w\in W^I$. By the directedness in [F4] there is $z\in W$ with $u\le z$ and $w\le z$; applying the order-preserving projection of step 2.1 and using $P^I(u)=u$, $P^I(w)=w$ (step 1.2) gives $u,w\le P^I(z)\in W^I$, so $W^I$ is directed. If $W^I$ is finite, directedness combines pairwise upper bounds to give $z_0\in W^I$ with $x\le z_0$ for every $x\in W^I$: start from a common upper bound of two elements and replace it by a common upper bound of it and a further element, finitely many times. Then $z_0$ is the maximum of $W^I$, it is unique because two maxima bound each other and $\le$ is antisymmetric, and $W^I=[1,z_0{]}^I$ by [F3] and the definition of $z_0$. No longest element of $W$ or of $W_I$ is used: [F1] and [F2] hold for arbitrary (possibly infinite) $W$, and in the infinite case the argument stops at directedness and asserts no maximum.

For (3), let $u,w\in W^I$ with $u<w$; choose a reduced expression $w=s_1\cdots s_q$ and a reduced subword expression of $u$ inside it, written in deleted-position form with deleted positions $D=\{i_1<\cdots <i_k\}$ and $i_k$ minimal, and let $x_1:=ut$ for the reflection $t$ produced by the augmentation lemma [F7]: then $u\to x_1$, $\mathrm{\ell }(x_1)=\mathrm{\ell }(u)+1$, and $x_1$ is the product of the word $W^{\mathrm{\prime }}$ obtained from $s_1\cdots s_q$ by deleting only $i_1,\dots ,i_{k-1}$, which is a reduced expression of $x_1$; in particular $x_1\le w$ by the subword criterion [F6]. We claim $x_1\in W^I$: if not, then part (2), proved in step 3.1, applied to the cover $u<x_1$ with $u\in W^I$ (the pair is a cover by the criterion [F8], since $u\to x_1$ and $\mathrm{\ell }(x_1)=\mathrm{\ell }(u)+1$) gives $x_1=us$ for some $s\in I$; but $x_1=ut$ then forces $t=s\in I$, and computing as in the augmentation lemma's construction gives $wt=(s_1\cdots s_q)(s_q\cdots s_{i_k+1})s_{i_k}(s_{i_k+1}\cdots s_q)=s_1\cdots \widehat{s_{i_k}}\cdots s_q$, a word of length $q-1$, so $\mathrm{\ell }(wt)<\mathrm{\ell }(w)$; since $t=s\in I$, this contradicts $w\in W^I$, which requires $\mathrm{\ell }(ws)>\mathrm{\ell }(w)$ for every $s\in I$. Hence $x_1\in W^I$.

For (3), induct on the gap $\mathrm{\ell }(w)-\mathrm{\ell }(u)$ over pairs $u\le w$ in $W^I$: the case $u=w$ is the one-element chain, and for $u<w$ step 4.1 produces $x_1\in W^I$ with $u\to x_1$, $\mathrm{\ell }(x_1)=\mathrm{\ell }(u)+1$ and $x_1$ the product of a reduced subword expression of the same word $s_1\cdots s_q$, so the induction hypothesis applies to the pair $(x_1,w)$ and yields a chain $x_1<\cdots <x_k=w$ in $W^I$ with lengths $\mathrm{\ell }(u)+2,\dots ,\mathrm{\ell }(w)$; prepending $x_0:=u$ gives the asserted chain, and $k=\mathrm{\ell }(w)-\mathrm{\ell }(u)$. Any strict step of a chain in $[u,w{]}^I$ strictly increases the length by [F3], so such a chain has at most $\mathrm{\ell }(w)-\mathrm{\ell }(u)$ strict steps; if it had fewer, some step $x_{i-1}<x_i$ would satisfy $\mathrm{\ell }(x_i)-\mathrm{\ell }(x_{i-1})\ge 2$, and step 4.1 applied to the pair $x_{i-1}<x_i$ (both in $W^I$, with the required reduced subword expression supplied by the subword criterion [F6]) would insert an element of $W^I$ strictly between them, so the chain would not be maximal; hence every maximal chain has exactly $\mathrm{\ell }(w)-\mathrm{\ell }(u)$ steps and the rank function $x\mapsto \mathrm{\ell }(x)-\mathrm{\ell }(u)$ is well defined on $[u,w{]}^I$; finally $[u,w{]}^I\subseteq [u,w]$ is finite by [F5].

Collecting: (1) is steps 1.1, 1.2 and 2.1, giving both the minimality $P^I(w)\le w$ with its equality case and order-preservation; (2) is step 3.1; (3) is steps 4.1 and 5.1, where the extra check $x_1\in W^I$ is the point at which the quotient does not simply inherit the chain property; and (4) is step 3.2. The infinite case is covered by the same steps, with no longest element asserted. No use of the Axiom of Choice is made: the chosen description, the common upper bound in step 3.2 and the induction of step 5.1 are all finite or deterministic constructs on the fixed group $W$.