let I be non empty set ; :: thesis: for M being ManySortedSet of I
for a, b being Element of ()
for A, B being Equivalence_Relation of M st a = A & b = B holds
( a [= b iff A c= B )

let M be ManySortedSet of I; :: thesis: for a, b being Element of ()
for A, B being Equivalence_Relation of M st a = A & b = B holds
( a [= b iff A c= B )

let a, b be Element of (); :: thesis: for A, B being Equivalence_Relation of M st a = A & b = B holds
( a [= b iff A c= B )

let A, B be Equivalence_Relation of M; :: thesis: ( a = A & b = B implies ( a [= b iff A c= B ) )
assume that
A1: a = A and
A2: b = B ; :: thesis: ( a [= b iff A c= B )
thus ( a [= b implies A c= B ) :: thesis: ( A c= B implies a [= b )
proof
assume A3: a [= b ; :: thesis: A c= B
A (/\) B = the L_meet of () . (A,B) by MSUALG_5:def 5
.= a "/\" b by
.= A by ;
hence A c= B by PBOOLE:15; :: thesis: verum
end;
thus ( A c= B implies a [= b ) :: thesis: verum
proof
assume A4: A c= B ; :: thesis: a [= b
a "/\" b = the L_meet of () . (A,B) by
.= A (/\) B by MSUALG_5:def 5
.= a by ;
hence a [= b by LATTICES:4; :: thesis: verum
end;