let S1, S2 be strict Lattice; ( ( 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 )
; S1 = S2
reconsider Z = the carrier of S1 as non empty set ;
then A36:
the carrier of S1 = the carrier of S2
by TARSKI:2;
A37:
now 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;
( 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
;
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
;
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; verum