let I be non empty set ; :: thesis: for M being ManySortedSet of I holds Top (EqRelLatt M) = [|M,M|]

let M be ManySortedSet of I; :: thesis: Top (EqRelLatt M) = [|M,M|]

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 M be ManySortedSet of I; :: thesis: Top (EqRelLatt M) = [|M,M|]

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;

now :: thesis: for a being Element of (EqRelLatt M) holds

( K "\/" a = K & a "\/" K = K )

hence
Top (EqRelLatt M) = [|M,M|]
by LATTICES:def 17; :: thesis: verum( K "\/" a = K & a "\/" K = K )

let a be Element of (EqRelLatt M); :: thesis: ( K "\/" a = K & a "\/" K = K )

reconsider K9 = K, a9 = a as Equivalence_Relation of M by MSUALG_5:def 5;

.= K9 "\/" a9 by MSUALG_5:def 5

.= K by A1, PBOOLE:3 ; :: thesis: a "\/" K = K

hence a "\/" K = K ; :: thesis: verum

end;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

thus K "\/" a =
the L_join of (EqRelLatt M) . (K,a)
by LATTICES:def 1
(K9 "\/" a9) . i = K9 . i

let i be object ; :: thesis: ( i in I implies (K9 "\/" a9) . i = K9 . i )

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: (K9 "\/" a9) . i = K9 . i

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: verum

end;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: (K9 "\/" a9) . i = K9 . i

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: verum

.= K9 "\/" a9 by MSUALG_5:def 5

.= K by A1, PBOOLE:3 ; :: thesis: a "\/" K = K

hence a "\/" K = K ; :: thesis: verum