let I be non empty set ; for M being ManySortedSet of I
for X being Subset of
for X1 being SubsetFamily of st X1 = X & not X is empty holds
meet |:X1:| is Equivalence_Relation of M
let M be ManySortedSet of I; for X being Subset of
for X1 being SubsetFamily of st X1 = X & not X is empty holds
meet |:X1:| is Equivalence_Relation of M
let X be Subset of ; for X1 being SubsetFamily of st X1 = X & not X is empty holds
meet |:X1:| is Equivalence_Relation of M
let X1 be SubsetFamily of ; ( X1 = X & not X is empty implies meet |:X1:| is Equivalence_Relation of M )
set a = meet |:X1:|;
then reconsider a = meet |:X1:| as ManySortedRelation of M by MSUALG_4:def 2;
assume that
A2:
X1 = X
and
A3:
not X is empty
; meet |:X1:| is Equivalence_Relation of M
now reconsider X1' =
X1 as non
empty SubsetFamily of
by A2, A3;
let i be
set ;
for R being Relation of st i in I & a . i = R holds
R is Equivalence_Relation of let R be
Relation of ;
( i in I & a . i = R implies R is Equivalence_Relation of )assume that A4:
i in I
and A5:
a . i = R
;
R is Equivalence_Relation of reconsider i' =
i as
Element of
I by A4;
reconsider b =
|:X1:| . i' as
Subset-Family of
by PBOOLE:def 21;
consider Q being
Subset-Family of
such that A6:
Q = |:X1:| . i
and A7:
R = Intersect Q
by A4, A5, MSSUBFAM:def 2;
reconsider Q =
Q as
Subset-Family of
by A4, PBOOLE:def 21;
|:X1':| is
non-empty
;
then A8:
Q <> {}
by A4, A6, PBOOLE:def 16;
A9:
|:X1':| . i = { (x . i) where x is Element of Bool [|M,M|] : x in X1 }
by A4, CLOSURE2:15;
now let Y be
set ;
( Y in b implies Y is Equivalence_Relation of )assume
Y in b
;
Y is Equivalence_Relation of 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 23;
then
z . i c= [|M,M|] . i
by A4, PBOOLE:def 5;
then reconsider Y1 =
Y as
Relation of
by A4, A10, PBOOLE:def 21;
z is
Equivalence_Relation of
M
by A11, MSUALG_5:def 5;
then
Y1 is
Equivalence_Relation of
by A4, A10, MSUALG_4:def 3;
hence
Y is
Equivalence_Relation of
;
verum end; then
meet b is
Equivalence_Relation of
by A6, A8, EQREL_1:19;
hence
R is
Equivalence_Relation of
by A6, A7, A8, SETFAM_1:def 10;
verum end;
hence
meet |:X1:| is Equivalence_Relation of M
by MSUALG_4:def 3; verum