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 ) )

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

hence
EqRelLatt M is complete
by VECTSP_8:def 6; :: thesis: verum
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;

end;( 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 )
;

end;

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 ) )

( 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;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

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 ) )

( 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 ) )

b [= a

b [= a ; :: thesis: verum

end;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

hence
a is_less_than X
; :: thesis: for b being Element of (EqRelLatt M) st b is_less_than 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;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

b [= a

now :: thesis: for b being Element of (EqRelLatt M) st b is_less_than X holds

b [= a

hence
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

hence b [= a by Th6; :: thesis: verum

end;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

then
b9 c= meet |:X1:|
by PBOOLE:def 2;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;

hence b9 . i c= (meet |:X1:|) . i by A6, A5, SETFAM_1:def 9; :: thesis: verum

end;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

then
b9 . i c= meet (|:X1:| . i)
by A6, SETFAM_1:5;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;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

hence b9 . i c= (meet |:X1:|) . i by A6, A5, SETFAM_1:def 9; :: thesis: verum

hence b [= a by Th6; :: thesis: verum

b [= a ; :: thesis: verum