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