let Y be set ; :: thesis: for X being Subset of (EqRelLatt Y)
for R being Relation of Y st R = union X holds
"\/" X = EqCl R
let X be Subset of (EqRelLatt Y); :: thesis: for R being Relation of Y st R = union X holds
"\/" X = EqCl R
let R be Relation of Y; :: thesis: ( R = union X implies "\/" X = EqCl R )
reconsider X1 = "\/" X as Equivalence_Relation of Y by MSUALG_5:21;
assume A1: R = union X ; :: thesis: "\/" X = EqCl R
A2: now :: thesis: for EqR being Equivalence_Relation of Y st R c= EqR holds
X1 c= EqR
let EqR be Equivalence_Relation of Y; :: thesis: ( R c= EqR implies X1 c= EqR )
reconsider EqR1 = EqR as Element of (EqRelLatt Y) by MSUALG_5:21;
assume A3: R c= EqR ; :: thesis: X1 c= EqR
now :: thesis: for q being Element of (EqRelLatt Y) st q in X holds
q [= EqR1
let q be Element of (EqRelLatt Y); :: thesis: ( q in X implies q [= EqR1 )
reconsider q1 = q as Equivalence_Relation of Y by MSUALG_5:21;
assume A4: q in X ; :: thesis: q [= EqR1
now :: thesis: for x being object st x in q1 holds
x in EqR
let x be object ; :: thesis: ( x in q1 implies x in EqR )
assume x in q1 ; :: thesis: x in EqR
then x in union X by A4, TARSKI:def 4;
hence x in EqR by A1, A3; :: thesis: verum
end;
then q1 c= EqR ;
hence q [= EqR1 by Th2; :: thesis: verum
end;
then X is_less_than EqR1 by LATTICE3:def 17;
then "\/" X [= EqR1 by LATTICE3:def 21;
hence X1 c= EqR by Th2; :: thesis: verum
end;
R c= "\/" X by A1, Th7;
hence "\/" X = EqCl R by A2, MSUALG_5:def 1; :: thesis: verum