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 ;

now :: thesis: for x being object holds
( 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;

then A36: the carrier of S1 = the carrier of S2 by TARSKI:2;

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) )

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;

then the L_meet of S1 = the L_meet of S2 by A36, BINOP_1:2;
hence S1 = S2 by A36, A37, BINOP_1:2; :: thesis: verum