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
A28: for x being set holds
( x in the carrier of S1 iff x is Equivalence_Relation of M ) and
A29: 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
A30: for x being set holds
( x in the carrier of S2 iff x is Equivalence_Relation of M ) and
A31: 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

A32: now

let x be set ; :: 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 A30;
hence ( x in the carrier of S1 iff x in the carrier of S2 ) by A28; :: thesis: verum

end;

then A33: the carrier of S1 = the carrier of S2 by TARSKI:2;
reconsider Z = the carrier of S1 as non empty set ;

now

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 A28;
thus the L_meet of S1 . x,y = x1 /\ y1 by A29
.= the L_meet of S2 . x,y by A31 ; :: 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 A29
.= the L_join of S2 . x,y by A31 ; :: thesis: verum

end;

then ( the L_meet of S1 = the L_meet of S2 & the L_join of S1 = the L_join of S2 ) by A33, BINOP_1:2;
hence S1 = S2 by A32, TARSKI:2; :: thesis: verum