let Y be set ; :: thesis: for X being Subset of (EqRelLatt Y) holds union X is Relation of Y
let X be Subset of (EqRelLatt Y); :: thesis: union X is Relation of Y

now

let x be set ; :: thesis: ( x in union X implies x in [:Y,Y:] )
assume x in union X ; :: thesis: x in [:Y,Y:]
then consider X' being set such that
A1: ( x in X' & X' in X ) by TARSKI:def 4;
X' is Equivalence_Relation of Y by A1, MSUALG_7:1;
then consider y, z being set such that
A2: ( x = [y,z] & y in Y & z in Y ) by A1, RELSET_1:6;
thus x in [:Y,Y:] by A2, ZFMISC_1:106; :: thesis: verum

end;

then union X c= [:Y,Y:] by TARSKI:def 3;
hence union X is Relation of Y ; :: thesis: verum