for Z being set st Z <> {} & Z is finite & ( for X, Y being set st X in Z & Y in Z & not X c= Y holds
Y c= X ) holds
union Z in Z by Lm6;