let Y be set ; :: thesis: EqRelLatt Y is complete
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: 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 ) )

per cases ( X is empty or not X is empty ) ;

suppose A1: X is empty ; :: thesis: 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 ) )

take a = Top (EqRelLatt Y); :: thesis: ( a is_less_than X & ( for b being Element of (EqRelLatt Y) st b is_less_than X holds
b [= a ) )
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: for b being Element of (EqRelLatt Y) st b is_less_than X holds
b [= a
let b be Element of (EqRelLatt Y); :: thesis: ( b is_less_than X implies b [= a )
assume b is_less_than X ; :: thesis: b [= a
thus b [= a by LATTICES:19; :: thesis: verum

end;

suppose A2: not X is empty ; :: thesis: 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 ) )

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

proof

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

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: ( a is_less_than X & ( for b being Element of (EqRelLatt Y) st b is_less_than X holds
b [= a ) )

now :: thesis: for q being Element of (EqRelLatt Y) st q in X holds
a [= q

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

end;

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

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

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

now :: thesis: for x being object st x in b9 holds
x in meet X

let x be object ; :: thesis: ( x in b9 implies x in meet X )
assume A4: x in b9 ; :: thesis: x in meet X

now :: thesis: for Z being set st Z in X holds
x in Z

let Z be set ; :: thesis: ( Z in X implies x in Z )
assume A5: Z in X ; :: thesis: x in Z
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: verum

end;

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

end;

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

end;

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

end;

end;

end;

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