let A be Ordinal; :: thesis: for X being set st X c= A holds
union X is Ordinal
let X be set ; :: thesis: ( X c= A implies union X is Ordinal )
assume X c= A ; :: thesis: union X is Ordinal
then for x being set st x in X holds
x is Ordinal ;
hence union X is Ordinal by ORDINAL1:35; :: thesis: verum