let I be non empty set ; :: thesis: for M being ManySortedSet of I

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 I; :: 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 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 )

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 I; :: 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 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

thus
( A c= B implies a [= b )
:: thesis: verum
assume A3:
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, A2, LATTICES:def 2

.= A by A1, A3, LATTICES:4 ;

hence A c= B by PBOOLE:15; :: thesis: verum

end;A (/\) B = the L_meet of (EqRelLatt M) . (A,B) by MSUALG_5:def 5

.= a "/\" b by A1, A2, LATTICES:def 2

.= A by A1, A3, LATTICES:4 ;

hence A c= B by PBOOLE:15; :: thesis: verum

proof

assume A4:
A c= B
; :: thesis: a [= b

a "/\" b = the L_meet of (EqRelLatt M) . (A,B) by A1, A2, LATTICES:def 2

.= A (/\) B by MSUALG_5:def 5

.= a by A1, A4, PBOOLE:23 ;

hence a [= b by LATTICES:4; :: thesis: verum

end;a "/\" b = the L_meet of (EqRelLatt M) . (A,B) by A1, A2, LATTICES:def 2

.= A (/\) B by MSUALG_5:def 5

.= a by A1, A4, PBOOLE:23 ;

hence a [= b by LATTICES:4; :: thesis: verum