## 3. 8 ORD(Order Exchange of Quantitization Symbols)

The exchanges between all of the successive symbols, or among the exist
symbols (ORD is an abbreviation of order).

Example 1 a1 : (All x) (All y) (Exist z) (Exist u) (f(x,y,z,u)) by ....
;

..........
a2 : (All y) (All x) (Exist u) (Exist z) (f(x,y,z,u)) by ORD (a1) ;
In the examples above, x, y, z, and u of both formulas a1 and a2 have
to be in the same line of letters. In THEAX, (All w) (f(w)) and (All px)
(f(px)) are generally considered to be the same formulas; however, ORD
does not allow such identicality.

If we take the following detour, this rule will not be needed; however,
the demonstration will be concise with it. It becomes the formula desired
by a8 (a1 is the same with above).

a2 : (All y) (All x) (;
a3 : (Exist z) (Exist u) (f(x,y,z,u)) by ALS(a1) ;
a4 : (Exist p) (Exist q) (;
a5 : f(x,y,p,q) by FLW (a1) ;
a6 : (Exist u) (Exist z) (f(x,y,z,u)) by EXIST (a5) ;
) ;

a7 : (Exist u) (Exist z) (f (x,y,z,u)) by CNST (a4) ;/*CNST will be
explained later*/) ;
a8 : (All y) (All x) (Exist u) (Exist z) (f(x,y,z,u)) by ARRN (a2)
;