for phi being Ordinal-Sequence
for A being Ordinal st phi is increasing holds
phi " A is epsilon-transitive epsilon-connected set