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: 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 Th5;
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 ; :: 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:19; :: 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 Th8;
set a9 = 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 :: thesis: for q being Element of (EqRelLatt M) st q in X holds
a [= q
let q be Element of (EqRelLatt M); :: 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 (EqRelLatt M) st b is_less_than X holds
b [= a
now :: 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 )
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 A4, PBOOLE:def 13;
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 A4, CLOSURE2:14;
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 (EqRelLatt M) 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 A4, A8, PBOOLE:def 2; :: thesis: verum
end;
then b9 . i c= meet (|:X1:| . i) by A6, SETFAM_1:5;
hence b9 . i c= (meet |:X1:|) . i by A6, A5, SETFAM_1:def 9; :: 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 (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