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

reconsider X1 = X as SubsetFamily of [|M,M|] by Th5;
per cases ( X is empty or not X is empty ) ;
suppose A1: X is empty ; :: thesis: ex a being Element of () st
( a is_less_than X & ( for b being Element of () st b is_less_than X holds
b [= a ) )

take a = Top (); :: thesis: ( a is_less_than X & ( for b being Element of () st b is_less_than X holds
b [= a ) )

for q being Element of () st q in X holds
a [= q by A1;
hence a is_less_than X ; :: thesis: for b being Element of () st b is_less_than X holds
b [= a

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

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

now :: thesis: for q being Element of () st q in X holds
a [= q
let q be Element of (); :: thesis: ( q in X implies a [= q )
reconsider q9 = q as Equivalence_Relation of M by MSUALG_5:def 5;
assume q in X ; :: thesis: a [= q
then a c= q9 by Th7;
hence a [= q by Th6; :: thesis: verum
end;
hence a is_less_than X ; :: thesis: for b being Element of () st b is_less_than X holds
b [= a

now :: thesis: for b being Element of () st b is_less_than X holds
b [= a
let b be Element of (); :: thesis: ( b is_less_than X implies b [= a )
reconsider b9 = b as Equivalence_Relation of M by MSUALG_5:def 5;
assume A3: b is_less_than X ; :: thesis: b [= a
now :: thesis: for i being object st i in I holds
b9 . i c= (meet |:X1:|) . i
reconsider X19 = X1 as non empty SubsetFamily of [|M,M|] by A2;
let i be object ; :: thesis: ( i in I implies b9 . i c= (meet |:X1:|) . i )
assume A4: i in I ; :: thesis: b9 . i c= (meet |:X1:|) . i
then A5: ex Q being Subset-Family of ([|M,M|] . i) st
( Q = |:X1:| . i & (meet |:X1:|) . i = Intersect Q ) by MSSUBFAM:def 1;
|:X19:| is V2() ;
then A6: |:X1:| . i <> {} by ;
now :: thesis: for Z being set st Z in |:X1:| . i holds
b9 . i c= Z
let Z be set ; :: thesis: ( Z in |:X1:| . i implies b9 . i c= Z )
assume A7: Z in |:X1:| . i ; :: thesis: b9 . i c= Z
|:X19:| . i = { (x . i) where x is Element of Bool [|M,M|] : x in X1 } by ;
then consider z being Element of Bool [|M,M|] such that
A8: Z = z . i and
A9: z in X1 by A7;
reconsider z9 = z as Element of () by A9;
reconsider z99 = z9 as Equivalence_Relation of M by MSUALG_5:def 5;
b [= z9 by A3, A9;
then b9 c= z99 by Th6;
hence b9 . i c= Z by ; :: thesis: verum
end;
then b9 . i c= meet (|:X1:| . i) by ;
hence b9 . i c= (meet |:X1:|) . i by ; :: thesis: verum
end;
then b9 c= meet |:X1:| by PBOOLE:def 2;
hence b [= a by Th6; :: thesis: verum
end;
hence for b being Element of () 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