Continuous nonalgebraic unit interval (source code)

= Continuous nonalgebraic unit interval
{title2=$x\ll y\iff x<y\text{ or }x=y=0$}

Give the <real interval> $[0,1]$ its usual <total order>. Every nonempty <directed set> has a <least upper bound> in the <real interval>, so it is a <directed-complete partial order>. If $x<y\leq\sup D$, some $d\in D$ exceeds $x$; otherwise $x$ would be an <upper bound> for $D$. Also $0\ll0$, since every member of a nonempty $D$ is at least zero. For $x>0$, the increasing <sequence> $x(1-1/n)$, $n\geq1$, has <least upper bound> $x$ but never reaches it, so $x\not\ll x$. Together with $x\ll y\Rightarrow x\leq y$, this proves the displayed <way-below relation>.

For each $y>0$, the elements <way-below> $y$ form $[0,y)$, a <directed set> with <least upper bound> $y$; for $y=0$ they form $\{0\}$. Thus this is a <continuous poset>. Its only <compact element> is zero, so it is not an <algebraic partially ordered set>.