:: deftheorem Def23 defines Euclidean AOFA_I00:def 23 :
for A being preIfWhileAlgebra holds
( A is Euclidean iff for X being non empty countable set
for T being Subset of (Funcs (X,INT)) ex f being ExecutionFunction of A, Funcs (X,INT),T st f is Euclidean );