\import{topology/topological-space.tex}
\import{order/order.tex}

\section{Order Topology}

\begin{abbreviation}\label{open_interval}
    $z \in \oointervalof{x}{y}$ iff $x \mathrel{R} y$ and $x \mathrel{R} z$ and $z \mathrel{R} y$.
    %$\oointervalof{x}{y}{X} = \{ z \mid x \in X, y \in X, z \in X x \mathrel{R} y \wedge x \mathrel{R} z \wedge z \mathrel{R} y\}$. 
\end{abbreviation}

\begin{struct}\label{order_topology}
    A ordertopology space $X$ is a onesorted structure equipped with
    \begin{enumerate}
        \item $<$
    \end{enumerate}
    such that 
    \begin{enumerate}
        \item \label{order_topology_1} $<$ is a strict order on $X$
        \item \label{order_topology_2}  
        \item \label{order_topology_3}
        \item \label{order_topology_4}
        \item \label{order_topology}
        \item \label{order_topology}
        \item \label{order_topology}
    \end{enumerate}
\end{struct}



%\begin{definition}\label{order_topology}
%    $X$ has the order topology iff for all $x,y \in X$ $X$ has a strict order $R$ and $\oointervalof{x}{y}{X} \in \opens[X]$ and $X$ is a topological space.
%    %$O$ is the order Topology on $X$ iff for all $x,y \in X$ $X$ has a strict order $R$ and $(x,y) \in O$ and $O$ is . 
%\end{definition}