Separative quotient and compatibility

If $p\le q$, every $r\le p$ itself witnesses compatibility with $q$; hence $p{\le }^{\ast }q$. In particular ${\le }^{\ast }$ is reflexive. If $p{\le }^{\ast }q{\le }^{\ast }s$ and $r\le p$, take $t\le r,q$ using the first relation. Since $t\le q$, the second relation gives $u\le t,s$. Then $u\le r,s$, proving $r$ compatible with $s$. As $r$ was arbitrary, $p{\le }^{\ast }s$, proving transitivity. Mutual ${\le }^{\ast }$ is therefore reflexive, symmetric and transitive. By F2 its classes form a set. If $p^{\mathrm{\prime }}\sim p$, $q^{\mathrm{\prime }}\sim q$ and $p{\le }^{\ast }q$, transitivity gives $p^{\mathrm{\prime }}{\le }^{\ast }p{\le }^{\ast }q{\le }^{\ast }{q}^{\mathrm{\prime }}$; the reverse replacement follows by reversing the equivalences. Thus the quotient order is well-defined. Reflexivity and transitivity descend, and mutual quotient inequalities give equal classes by the definition of $\sim$, proving antisymmetry.

If $p,q$ have an original common extension $r$, step 1.1 gives $[r]⪯[p],[q]$. Conversely, suppose $[r]⪯[p],[q]$. Since $r\le r$ and $r{\le }^{\ast }p$, take $s\le r,p$. The relation $r{\le }^{\ast }q$ applied to $s\le r$ gives $t\le s,q$, so $t\le p,q$. Thus quotient compatibility is equivalent to original compatibility. In particular incompatibility is also preserved and reflected; no representatives of all classes were selected, only a representative of the one class under discussion.

If $[p]⋠[q]$, negating the defining universal statement supplies $r\le p$ incompatible with $q$. Then $[r]⪯[p]$ by step 1.1 and $[r]$ is incompatible with $[q]$ by step 2.1. This proves separativity. If the original partial order is separative and $p\nleqq q$, its separating extension witnesses $p{\nleqq }^{\ast }q$; combined with step 1.1 this gives ${\le }^{\ast }=\le$. Antisymmetry then makes each equivalence class a singleton, so the quotient map is an order isomorphism. The quotient is nonempty because $P$ is nonempty. A singleton preorder gives a singleton quotient; no greatest or least condition was used. QED.