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 10;
hence union (On X) is Ordinal by ORDINAL1:35; :: thesis: verum