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

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' and
A2: X' in X by TARSKI:def 4;
X' is Equivalence_Relation of by A2, MSUALG_7:1;
hence x in [:Y,Y:] by A1; :: thesis: verum

end;

hence union X is Relation of by TARSKI:def 3; :: thesis: verum