let Y be set ; :: thesis: for X being Subset of (EqRelLatt Y) holds union X c= "\/" X
let X be Subset of (EqRelLatt Y); :: thesis: union X c= "\/" X
reconsider X' = "\/" X as Equivalence_Relation of Y by MSUALG_7:1;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in union X or x in "\/" X )
assume x in union X ; :: thesis: x in "\/" X
then consider X1 being set such that
A1: ( x in X1 & X1 in X ) by TARSKI:def 4;
reconsider X1 = X1 as Element of (EqRelLatt Y) by A1;
reconsider X2 = X1 as Equivalence_Relation of Y by MSUALG_7:1;
X is_less_than "\/" X by LATTICE3:def 21;
then X1 [= "\/" X by A1, LATTICE3:def 17;
then X2 c= X' by Th2;
hence x in "\/" X by A1; :: thesis: verum