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