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 :: thesis: for x being object st x in union X holds
x in [:Y,Y:]
let x be object ; :: thesis: ( x in union X implies x in [:Y,Y:] )
assume x in union X ; :: thesis: x in [:Y,Y:]
then consider X9 being set such that
A1: x in X9 and
A2: X9 in X by TARSKI:def 4;
X9 is Equivalence_Relation of Y by A2, MSUALG_5:21;
hence x in [:Y,Y:] by A1; :: thesis: verum
end;
hence union X is Relation of Y by TARSKI:def 3; :: thesis: verum