let S1, S2 be strict Lattice; :: thesis: ( ( for x being set holds

( x in the carrier of S1 iff x is Equivalence_Relation of M ) ) & ( for x, y being Equivalence_Relation of M holds

( the L_meet of S1 . (x,y) = x (/\) y & the L_join of S1 . (x,y) = x "\/" y ) ) & ( for x being set holds

( x in the carrier of S2 iff x is Equivalence_Relation of M ) ) & ( for x, y being Equivalence_Relation of M holds

( the L_meet of S2 . (x,y) = x (/\) y & the L_join of S2 . (x,y) = x "\/" y ) ) implies S1 = S2 )

assume that

A32: for x being set holds

( x in the carrier of S1 iff x is Equivalence_Relation of M ) and

A33: for x, y being Equivalence_Relation of M holds

( the L_meet of S1 . (x,y) = x (/\) y & the L_join of S1 . (x,y) = x "\/" y ) and

A34: for x being set holds

( x in the carrier of S2 iff x is Equivalence_Relation of M ) and

A35: for x, y being Equivalence_Relation of M holds

( the L_meet of S2 . (x,y) = x (/\) y & the L_join of S2 . (x,y) = x "\/" y ) ; :: thesis: S1 = S2

reconsider Z = the carrier of S1 as non empty set ;

hence S1 = S2 by A36, A37, BINOP_1:2; :: thesis: verum

( x in the carrier of S1 iff x is Equivalence_Relation of M ) ) & ( for x, y being Equivalence_Relation of M holds

( the L_meet of S1 . (x,y) = x (/\) y & the L_join of S1 . (x,y) = x "\/" y ) ) & ( for x being set holds

( x in the carrier of S2 iff x is Equivalence_Relation of M ) ) & ( for x, y being Equivalence_Relation of M holds

( the L_meet of S2 . (x,y) = x (/\) y & the L_join of S2 . (x,y) = x "\/" y ) ) implies S1 = S2 )

assume that

A32: for x being set holds

( x in the carrier of S1 iff x is Equivalence_Relation of M ) and

A33: for x, y being Equivalence_Relation of M holds

( the L_meet of S1 . (x,y) = x (/\) y & the L_join of S1 . (x,y) = x "\/" y ) and

A34: for x being set holds

( x in the carrier of S2 iff x is Equivalence_Relation of M ) and

A35: for x, y being Equivalence_Relation of M holds

( the L_meet of S2 . (x,y) = x (/\) y & the L_join of S2 . (x,y) = x "\/" y ) ; :: thesis: S1 = S2

reconsider Z = the carrier of S1 as non empty set ;

now :: thesis: for x being object holds

( x in the carrier of S1 iff x in the carrier of S2 )

then A36:
the carrier of S1 = the carrier of S2
by TARSKI:2;( x in the carrier of S1 iff x in the carrier of S2 )

let x be object ; :: thesis: ( x in the carrier of S1 iff x in the carrier of S2 )

( x is Equivalence_Relation of M iff x in the carrier of S2 ) by A34;

hence ( x in the carrier of S1 iff x in the carrier of S2 ) by A32; :: thesis: verum

end;( x is Equivalence_Relation of M iff x in the carrier of S2 ) by A34;

hence ( x in the carrier of S1 iff x in the carrier of S2 ) by A32; :: thesis: verum

A37: now :: thesis: for x, y being Element of Z holds

( the L_meet of S1 . (x,y) = the L_meet of S2 . (x,y) & the L_join of S1 . (x,y) = the L_join of S2 . (x,y) )

then
the L_meet of S1 = the L_meet of S2
by A36, BINOP_1:2;( the L_meet of S1 . (x,y) = the L_meet of S2 . (x,y) & the L_join of S1 . (x,y) = the L_join of S2 . (x,y) )

let x, y be Element of Z; :: thesis: ( the L_meet of S1 . (x,y) = the L_meet of S2 . (x,y) & the L_join of S1 . (x,y) = the L_join of S2 . (x,y) )

reconsider x1 = x, y1 = y as Equivalence_Relation of M by A32;

thus the L_meet of S1 . (x,y) = x1 (/\) y1 by A33

.= the L_meet of S2 . (x,y) by A35 ; :: thesis: the L_join of S1 . (x,y) = the L_join of S2 . (x,y)

thus the L_join of S1 . (x,y) = x1 "\/" y1 by A33

.= the L_join of S2 . (x,y) by A35 ; :: thesis: verum

end;reconsider x1 = x, y1 = y as Equivalence_Relation of M by A32;

thus the L_meet of S1 . (x,y) = x1 (/\) y1 by A33

.= the L_meet of S2 . (x,y) by A35 ; :: thesis: the L_join of S1 . (x,y) = the L_join of S2 . (x,y)

thus the L_join of S1 . (x,y) = x1 "\/" y1 by A33

.= the L_join of S2 . (x,y) by A35 ; :: thesis: verum

hence S1 = S2 by A36, A37, BINOP_1:2; :: thesis: verum