ORDERS

Definition S.O.1 - Partial Order
(X,E) is a partially ordered set if and only if
E c XxX and 

(1) /\(x:-X) xEx,
(2) /\(x,y:-X) xEy and yEx => y = x,
(3) /\(x,y,z:-X) xEy and yEz => xEz.

Remark: If we write that 
(X,c) is a partlially ordered set
we mean that (X,E) is a partially ordered set where
E = {(A,B):-XxX)|A c B}.

Definition S.O.2 - Linear Order
(X,E) is a linearly ordered set if and only if
E c XxX and

(1) /\(x:-X) xEx,
(2) /\(x,y:-X) xEy and yEx => y = x,
(3) /\(x,y,z:-X) xEy and yEz => xEz,
(4) /\(x,y:-X) xEy or yEx.

Definition S.O.3 - Well Order
(X,E) is a well ordered set if and only if
E c XxX and

(1) /\(x:-X) xEx,
(2) /\(x,y:-X) xEy and yEx => y = x,
(3) /\(x,y,z:-X) xEy and yEz => xEz,
(4) /\(A) ( AcX and A != O => \/(y:-A)/\(z:-A) yEz ).

Theorem S.O.4
If (X,E) is a linearly ordered set then 
(X,E) is a partially ordered set.

Proof
It is true by Definition S.O.2 and Definition S.O.3.

Theorem S.O.5
If (X,E) is a well ordered set then
(X,E) is a linearly ordered set.

Proof
Take any a,b:-X.
Assume to the contrary that !(aEb) and !(bEa).
Let A = {a,b}.
Thus /\(z:-A) \/(y:-A) !(zRy). 
But by Definition S.O.3 we have 
\/(z:-A)/\(y:-A) zRy. Contradiction.
We have proved that aEb or bEa.

Definition S.O.6 - Initial Segment
Let (X,E) be a partially ordered set.
AcX is an initial segment of X if and only if
/\(a:-A)/\(x:-X) xEa => x:-A.

Theorem S.O.7
If (X,E) is a partially ordered set, KcP(x)
and /\(A:-K) A is an initial segment of X
then u(K) is an initial segment of X.

Proof
Take any a:-u(K).
Take any x:-X such that xEa.
We have A:-K such that a:-A.
Since A is an initial segment of X, x:-A.
Thus x:-u(K).
We have shown that u(K) is an initial segment of X.

Theorem S.O.8
If (X,E) is a well ordered set, AcX and A != X
then A is an initial segment of X if and only if
there is a z:-X such that
A = {x:-X | xEz and z!=x}.

Proof
Assume that there is a z:-X such that
A = {x:-X | xEz and z!=x}.
Take any a:-A.
Take any x:-X such that xEa.
By transitivity we have xEz and x!=z.
Thus x:-A. So A is an initial segment of X.

Now, assume that A is an initial segment of X.
By Definition S.O.3 we have z:-X\A such that
/\(y:-X\A) zEy.
It is obvious that {x:-X | xEz and z!=x} c A.
We will show that A c {x:-X | xEz and z!=x}.
Take any a:-A.
Assume to the contrary that zEa.
Then by Definition S.O.6 z:-A. Contradiction.
We have shown that !(zEa).
By Theorem S.O.5 (X,E) is a linearlly ordered set.
Thus aEz and z != a. So a:-{x:-X | xEz and z!=x}.
We have shown that A = {x:-X | xEz and z!=x}.
Now the proof is complete.