let Y be set ; :: thesis:
for X being Subset of (EqRelLatt Y) ex a being Element of (EqRelLatt Y) st
( a is_less_than X & ( for b being Element of (EqRelLatt Y) st b is_less_than X holds
b [= a ) )

proof

let X be Subset of (EqRelLatt Y); :: thesis:

per cases ;

suppose A1: X is empty ; :: thesis:

take a = Top (EqRelLatt Y); :: thesis:
for q being Element of (EqRelLatt Y) st q in X holds
a [= q by A1;
hence a is_less_than X by LATTICE3:def 16; :: thesis:
let b be Element of (EqRelLatt Y); :: thesis:
assume b is_less_than X ; :: thesis:
thus b [= a by LATTICES:19; :: thesis:

end;

suppose A2: not X is empty ; :: thesis:

set a = meet X;
X c= bool [:Y,Y:]

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in X ; :: thesis:
then x is Equivalence_Relation of Y by MSUALG_5:21;
hence x in bool [:Y,Y:] ; :: thesis:

end;

then reconsider X9 = X as Subset-Family of [:Y,Y:] ;
for Z being set st Z in X holds
Z is Equivalence_Relation of Y by MSUALG_5:21;
then meet X9 is Equivalence_Relation of Y by A2, EQREL_1:11;
then reconsider a = meet X as Equivalence_Relation of Y ;
set a9 = a;
reconsider a = a as Element of (EqRelLatt Y) by MSUALG_5:21;
take a ; :: thesis:

now :: thesis:

let q be Element of (EqRelLatt Y); :: thesis:
reconsider q9 = q as Equivalence_Relation of Y by MSUALG_5:21;
assume q in X ; :: thesis:
then a c= q9 by SETFAM_1:3;
hence a [= q by Th2; :: thesis:

end;

hence a is_less_than X by LATTICE3:def 16; :: thesis:

now :: thesis:

let b be Element of (EqRelLatt Y); :: thesis:
reconsider b9 = b as Equivalence_Relation of Y by MSUALG_5:21;
assume A3: b is_less_than X ; :: thesis:

now :: thesis:

let x be object ; :: thesis:
assume A4: x in b9 ; :: thesis:

now :: thesis:

let Z be set ; :: thesis:
assume A5: Z in X ; :: thesis:
then reconsider Z1 = Z as Element of (EqRelLatt Y) ;
reconsider Z9 = Z1 as Equivalence_Relation of Y by MSUALG_5:21;
b [= Z1 by A3, A5, LATTICE3:def 16;
then b9 c= Z9 by Th2;
hence x in Z by A4; :: thesis:

end;

hence x in meet X by A2, SETFAM_1:def 1; :: thesis:

end;

then b9 c= meet X ;
hence b [= a by Th2; :: thesis:

end;

hence for b being Element of (EqRelLatt Y) st b is_less_than X holds
b [= a ; :: thesis:

end;

end;

end;

hence EqRelLatt Y is complete by VECTSP_8:def 6; :: thesis: