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