let I be non empty set ; :: thesis: for M being ManySortedSet of I

for X being Subset of (EqRelLatt M)

for X1 being SubsetFamily of [|M,M|] st X1 = X & not X is empty holds

meet |:X1:| is Equivalence_Relation of M

let M be ManySortedSet of I; :: thesis: for X being Subset of (EqRelLatt M)

for X1 being SubsetFamily of [|M,M|] st X1 = X & not X is empty holds

meet |:X1:| is Equivalence_Relation of M

let X be Subset of (EqRelLatt M); :: thesis: for X1 being SubsetFamily of [|M,M|] st X1 = X & not X is empty holds

meet |:X1:| is Equivalence_Relation of M

let X1 be SubsetFamily of [|M,M|]; :: thesis: ( X1 = X & not X is empty implies meet |:X1:| is Equivalence_Relation of M )

set a = meet |:X1:|;

assume that

A2: X1 = X and

A3: not X is empty ; :: thesis: meet |:X1:| is Equivalence_Relation of M

for X being Subset of (EqRelLatt M)

for X1 being SubsetFamily of [|M,M|] st X1 = X & not X is empty holds

meet |:X1:| is Equivalence_Relation of M

let M be ManySortedSet of I; :: thesis: for X being Subset of (EqRelLatt M)

for X1 being SubsetFamily of [|M,M|] st X1 = X & not X is empty holds

meet |:X1:| is Equivalence_Relation of M

let X be Subset of (EqRelLatt M); :: thesis: for X1 being SubsetFamily of [|M,M|] st X1 = X & not X is empty holds

meet |:X1:| is Equivalence_Relation of M

let X1 be SubsetFamily of [|M,M|]; :: thesis: ( X1 = X & not X is empty implies meet |:X1:| is Equivalence_Relation of M )

set a = meet |:X1:|;

now :: thesis: for i being set st i in I holds

(meet |:X1:|) . i is Relation of (M . i)

then reconsider a = meet |:X1:| as ManySortedRelation of M by MSUALG_4:def 1;(meet |:X1:|) . i is Relation of (M . i)

let i be set ; :: thesis: ( i in I implies (meet |:X1:|) . i is Relation of (M . i) )

assume A1: i in I ; :: thesis: (meet |:X1:|) . i is Relation of (M . i)

meet |:X1:| c= [|M,M|] by PBOOLE:def 18;

then (meet |:X1:|) . i c= [|M,M|] . i by A1, PBOOLE:def 2;

hence (meet |:X1:|) . i is Relation of (M . i) by A1, PBOOLE:def 16; :: thesis: verum

end;assume A1: i in I ; :: thesis: (meet |:X1:|) . i is Relation of (M . i)

meet |:X1:| c= [|M,M|] by PBOOLE:def 18;

then (meet |:X1:|) . i c= [|M,M|] . i by A1, PBOOLE:def 2;

hence (meet |:X1:|) . i is Relation of (M . i) by A1, PBOOLE:def 16; :: thesis: verum

assume that

A2: X1 = X and

A3: not X is empty ; :: thesis: meet |:X1:| is Equivalence_Relation of M

now :: thesis: for i being set

for R being Relation of (M . i) st i in I & a . i = R holds

R is Equivalence_Relation of (M . i)

hence
meet |:X1:| is Equivalence_Relation of M
by MSUALG_4:def 2; :: thesis: verumfor R being Relation of (M . i) st i in I & a . i = R holds

R is Equivalence_Relation of (M . i)

reconsider X19 = X1 as non empty SubsetFamily of [|M,M|] by A2, A3;

let i be set ; :: thesis: for R being Relation of (M . i) st i in I & a . i = R holds

R is Equivalence_Relation of (M . i)

let R be Relation of (M . i); :: thesis: ( i in I & a . i = R implies R is Equivalence_Relation of (M . i) )

assume that

A4: i in I and

A5: a . i = R ; :: thesis: R is Equivalence_Relation of (M . i)

reconsider i9 = i as Element of I by A4;

reconsider b = |:X1:| . i9 as Subset-Family of [:(M . i),(M . i):] by PBOOLE:def 16;

consider Q being Subset-Family of ([|M,M|] . i) such that

A6: Q = |:X1:| . i and

A7: R = Intersect Q by A4, A5, MSSUBFAM:def 1;

reconsider Q = Q as Subset-Family of [:(M . i),(M . i):] by A4, PBOOLE:def 16;

|:X19:| is V2() ;

then A8: Q <> {} by A4, A6, PBOOLE:def 13;

A9: |:X19:| . i = { (x . i) where x is Element of Bool [|M,M|] : x in X1 } by A4, CLOSURE2:14;

hence R is Equivalence_Relation of (M . i) by A6, A7, A8, SETFAM_1:def 9; :: thesis: verum

end;let i be set ; :: thesis: for R being Relation of (M . i) st i in I & a . i = R holds

R is Equivalence_Relation of (M . i)

let R be Relation of (M . i); :: thesis: ( i in I & a . i = R implies R is Equivalence_Relation of (M . i) )

assume that

A4: i in I and

A5: a . i = R ; :: thesis: R is Equivalence_Relation of (M . i)

reconsider i9 = i as Element of I by A4;

reconsider b = |:X1:| . i9 as Subset-Family of [:(M . i),(M . i):] by PBOOLE:def 16;

consider Q being Subset-Family of ([|M,M|] . i) such that

A6: Q = |:X1:| . i and

A7: R = Intersect Q by A4, A5, MSSUBFAM:def 1;

reconsider Q = Q as Subset-Family of [:(M . i),(M . i):] by A4, PBOOLE:def 16;

|:X19:| is V2() ;

then A8: Q <> {} by A4, A6, PBOOLE:def 13;

A9: |:X19:| . i = { (x . i) where x is Element of Bool [|M,M|] : x in X1 } by A4, CLOSURE2:14;

now :: thesis: for Y being set st Y in b holds

Y is Equivalence_Relation of (M . i)

then
meet b is Equivalence_Relation of (M . i)
by A6, A8, EQREL_1:11;Y is Equivalence_Relation of (M . i)

let Y be set ; :: thesis: ( Y in b implies Y is Equivalence_Relation of (M . i) )

assume Y in b ; :: thesis: Y is Equivalence_Relation of (M . i)

then consider z being Element of Bool [|M,M|] such that

A10: Y = z . i and

A11: z in X by A2, A9;

z c= [|M,M|] by PBOOLE:def 18;

then z . i c= [|M,M|] . i by A4, PBOOLE:def 2;

then reconsider Y1 = Y as Relation of (M . i) by A4, A10, PBOOLE:def 16;

z is Equivalence_Relation of M by A11, MSUALG_5:def 5;

then Y1 is Equivalence_Relation of (M . i) by A4, A10, MSUALG_4:def 2;

hence Y is Equivalence_Relation of (M . i) ; :: thesis: verum

end;assume Y in b ; :: thesis: Y is Equivalence_Relation of (M . i)

then consider z being Element of Bool [|M,M|] such that

A10: Y = z . i and

A11: z in X by A2, A9;

z c= [|M,M|] by PBOOLE:def 18;

then z . i c= [|M,M|] . i by A4, PBOOLE:def 2;

then reconsider Y1 = Y as Relation of (M . i) by A4, A10, PBOOLE:def 16;

z is Equivalence_Relation of M by A11, MSUALG_5:def 5;

then Y1 is Equivalence_Relation of (M . i) by A4, A10, MSUALG_4:def 2;

hence Y is Equivalence_Relation of (M . i) ; :: thesis: verum

hence R is Equivalence_Relation of (M . i) by A6, A7, A8, SETFAM_1:def 9; :: thesis: verum