EXIST works just the opposite way from ALS. Each Example below corresponds with examples of ALS(§3. 3).
Example 1 a1 : f(a) by ....;
Example 2 a1 : f([c=d] , B(k) and B(k) (a) by....;..........
Example 3 a1 : u((All z) (t(z)), True) by ..;
Therefore, if we form a formula by substituting a formula of only registered names into variables, a formula made by restricting variables with exist symbols is also structured. This implies the opposet of ALS's case (in a sense that it quantitizes unquantitized formulas); however, in reality, work that the THEAX system conducts is also opposite of ALS's work. This is done by reversing the conditional formula (formula 1 of the example above) and the conclusion formula (formula 2 of the example above) before anything else and changing the new conditional formula (previous conclusion formula) of Exist into All. After that, we inspect if the conclusion formula (previous conditional formula) can be actually guided by using the routine of ALS.