let I be non empty set ; :: thesis: for M being ManySortedSet of
for a, b being Element of (EqRelLatt M)
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 ; :: thesis: for a, b being Element of (EqRelLatt M)
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 (EqRelLatt M); :: 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 A1: ( a = A & 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 A2: a [= b ; :: thesis: A c= B
A /\ B = the L_meet of (EqRelLatt M) . A,B by MSUALG_5:def 5
.= a "/\" b by A1, LATTICES:def 2
.= A by A1, A2, LATTICES:21 ;
hence A c= B by PBOOLE:17; :: thesis: verum

end;

thus ( A c= B implies a [= b ) :: thesis: verum

proof

assume A3: A c= B ; :: thesis: a [= b
a "/\" b = the L_meet of (EqRelLatt M) . A,B by A1, LATTICES:def 2
.= A /\ B by MSUALG_5:def 5
.= a by A1, A3, PBOOLE:25 ;
hence a [= b by LATTICES:21; :: thesis: verum

end;