let I be non empty set ; :: thesis:
let M be ManySortedSet of I; :: thesis:
set K = [|M,M|];
[|M,M|] is Equivalence_Relation of M by Th2;
then reconsider K = [|M,M|] as Element of (EqRelLatt M) by MSUALG_5:def 5;

let a be Element of (EqRelLatt M); :: thesis:
reconsider K9 = K, a9 = a as Equivalence_Relation of M by MSUALG_5:def 5;

let i be object ; :: thesis:
A2: ex K1 being ManySortedRelation of M st
( K1 = K9 (\/) a9 & K9 "\/" a9 = EqCl K1 ) by MSUALG_5:def 4;
assume A3: i in I ; :: thesis:
then reconsider i9 = i as Element of I ;
reconsider K2 = K9 . i9, a2 = a9 . i9 as Equivalence_Relation of (M . i) by MSUALG_4:def 2;
(K9 (\/) a9) . i = (K9 . i) \/ (a9 . i) by A3, PBOOLE:def 4
.= [:(M . i),(M . i):] \/ (a9 . i) by A3, PBOOLE:def 16
.= (nabla (M . i)) \/ a2 by EQREL_1:def 1
.= nabla (M . i) by EQREL_1:1
.= [:(M . i),(M . i):] by EQREL_1:def 1
.= K9 . i by A3, PBOOLE:def 16 ;
hence (K9 "\/" a9) . i = EqCl K2 by A2, MSUALG_5:def 3
.= K9 . i by MSUALG_5:2 ;
:: thesis:

end;

end;