let X be set ; :: thesis: union (On X) is epsilon-transitive epsilon-connected set
for x being object st x in On X holds
x is Ordinal by ORDINAL1:def 9;
hence union (On X) is epsilon-transitive epsilon-connected set by ORDINAL1:23; :: thesis: verum