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
A33: for x being set holds
( x in the carrier of S1 iff x is Equivalence_Relation of M ) and
A34: 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
A35: for x being set holds
( x in the carrier of S2 iff x is Equivalence_Relation of M ) and
A36: 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

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 A35;
hence ( x in the carrier of S1 iff x in the carrier of S2 ) by A33; :: thesis: verum

end;

then A37: the carrier of S1 = the carrier of S2 by TARSKI:1;

A38: 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 A33;
thus the L_meet of S1 . (x,y) = x1 /\ y1 by A34
.= the L_meet of S2 . (x,y) by A36 ; :: 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 A34
.= the L_join of S2 . (x,y) by A36 ; :: thesis: verum

end;

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