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 X9 = "\/" X as Equivalence_Relation of Y by MSUALG_5:21;
let x be object ; :: 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 and
A2: X1 in X by TARSKI:def 4;
reconsider X1 = X1 as Element of (EqRelLatt Y) by A2;
reconsider X2 = X1 as Equivalence_Relation of Y by MSUALG_5:21;
X is_less_than "\/" X by LATTICE3:def 21;
then X1 [= "\/" X by A2, LATTICE3:def 17;
then X2 c= X9 by Th2;
hence x in "\/" X by A1; :: thesis: verum