let I be non empty set ; :: thesis: for M being ManySortedSet of I holds Bottom () = id M
let M be ManySortedSet of I; :: thesis: Bottom () = id M
set K = id M;
id M is Equivalence_Relation of M by Th1;
then reconsider K = id M as Element of () by MSUALG_5:def 5;
now :: thesis: for a being Element of () holds
( K "/\" a = K & a "/\" K = K )
let a be Element of (); :: thesis: ( K "/\" a = K & a "/\" K = K )
reconsider K9 = K, a9 = a as Equivalence_Relation of M by MSUALG_5:def 5;
A1: now :: thesis: for i being object st i in I holds
(K9 (/\) a9) . i = K9 . i
let i be object ; :: thesis: ( i in I implies (K9 (/\) a9) . i = K9 . i )
assume A2: i in I ; :: thesis: (K9 (/\) a9) . i = K9 . i
then reconsider i9 = i as Element of I ;
reconsider a2 = a9 . i9 as Equivalence_Relation of (M . i) by MSUALG_4:def 2;
thus (K9 (/\) a9) . i = (K9 . i) /\ (a9 . i) by
.= (id (M . i)) /\ a2 by MSUALG_3:def 1
.= id (M . i) by EQREL_1:10
.= K9 . i by ; :: thesis: verum
end;
thus K "/\" a = the L_meet of () . (K,a) by LATTICES:def 2
.= K9 (/\) a9 by MSUALG_5:def 5
.= K by ; :: thesis: a "/\" K = K
hence a "/\" K = K ; :: thesis: verum
end;
hence Bottom () = id M by LATTICES:def 16; :: thesis: verum