let I be non empty set ; :: thesis: for M being ManySortedSet of holds EqRelLatt M is complete
let M be ManySortedSet of ; :: thesis: EqRelLatt M is complete
for X being Subset of (EqRelLatt M) ex a being Element of (EqRelLatt M) st
( a is_less_than X & ( for b being Element of (EqRelLatt M) st b is_less_than X holds
b [= a ) )

proof

let X be Subset of (EqRelLatt M); :: thesis: ex a being Element of (EqRelLatt M) st
( a is_less_than X & ( for b being Element of (EqRelLatt M) st b is_less_than X holds
b [= a ) )
reconsider X1 = X as SubsetFamily of [|M,M|] by Th6;

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

suppose A1: X is empty ; :: thesis: ex a being Element of (EqRelLatt M) st
( a is_less_than X & ( for b being Element of (EqRelLatt M) st b is_less_than X holds
b [= a ) )

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

end;

suppose A2: not X is empty ; :: thesis: ex a being Element of (EqRelLatt M) st
( a is_less_than X & ( for b being Element of (EqRelLatt M) st b is_less_than X holds
b [= a ) )

then reconsider a = meet |:X1:| as Equivalence_Relation of M by Th9;
set a' = a;
reconsider a = a as Element of (EqRelLatt M) by MSUALG_5:def 5;
take a ; :: thesis: ( a is_less_than X & ( for b being Element of (EqRelLatt M) st b is_less_than X holds
b [= a ) )

now

let q be Element of (EqRelLatt M); :: thesis: ( q in X implies a [= q )
reconsider q' = q as Equivalence_Relation of M by MSUALG_5:def 5;
assume q in X ; :: thesis: a [= q
then a c= q' by Th8;
hence a [= q by Th7; :: thesis: verum

end;

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

now

let b be Element of (EqRelLatt M); :: thesis: ( b is_less_than X implies b [= a )
reconsider b' = b as Equivalence_Relation of M by MSUALG_5:def 5;
assume A3: b is_less_than X ; :: thesis: b [= a

now

let i be set ; :: thesis: ( i in I implies b' . i c= (meet |:X1:|) . i )
assume A4: i in I ; :: thesis: b' . i c= (meet |:X1:|) . i
reconsider X1' = X1 as non empty SubsetFamily of [|M,M|] by A2;
|:X1':| is non-empty ;
then A5: |:X1:| . i <> {} by A4, PBOOLE:def 16;
consider Q being Subset-Family of ([|M,M|] . i) such that
A6: ( Q = |:X1:| . i & (meet |:X1:|) . i = Intersect Q ) by A4, MSSUBFAM:def 2;

now

let Z be set ; :: thesis: ( Z in |:X1:| . i implies b' . i c= Z )
assume A7: Z in |:X1:| . i ; :: thesis: b' . i c= Z
|:X1':| . i = { (x . i) where x is Element of Bool [|M,M|] : x in X1 } by A4, CLOSURE2:15;
then consider z being Element of Bool [|M,M|] such that
A8: ( Z = z . i & z in X1 ) by A7;
reconsider z' = z as Element of (EqRelLatt M) by A8;
reconsider z'' = z' as Equivalence_Relation of M by MSUALG_5:def 5;
b [= z' by A3, A8, LATTICE3:def 16;
then b' c= z'' by Th7;
hence b' . i c= Z by A4, A8, PBOOLE:def 5; :: thesis: verum

end;

then b' . i c= meet (|:X1:| . i) by A5, SETFAM_1:6;
hence b' . i c= (meet |:X1:|) . i by A5, A6, SETFAM_1:def 10; :: thesis: verum

end;

then b' c= meet |:X1:| by PBOOLE:def 5;
hence b [= a by Th7; :: thesis: verum

end;

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

end;

end;

end;

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