let P1, P2 be strict Lattice; ( the carrier of P1 = { x where x is Relation of X,X : x is Equivalence_Relation of X } & ( for x, y being Equivalence_Relation of X holds
( the L_meet of P1 . (x,y) = x /\ y & the L_join of P1 . (x,y) = x "\/" y ) ) & the carrier of P2 = { x where x is Relation of X,X : x is Equivalence_Relation of X } & ( for x, y being Equivalence_Relation of X holds
( the L_meet of P2 . (x,y) = x /\ y & the L_join of P2 . (x,y) = x "\/" y ) ) implies P1 = P2 )
assume that
A38:
the carrier of P1 = { x where x is Relation of X,X : x is Equivalence_Relation of X }
and
A39:
for x, y being Equivalence_Relation of X holds
( the L_meet of P1 . (x,y) = x /\ y & the L_join of P1 . (x,y) = x "\/" y )
and
A40:
the carrier of P2 = { x where x is Relation of X,X : x is Equivalence_Relation of X }
and
A41:
for x, y being Equivalence_Relation of X holds
( the L_meet of P2 . (x,y) = x /\ y & the L_join of P2 . (x,y) = x "\/" y )
; P1 = P2
reconsider Z = the carrier of P1 as non empty set ;
then A43:
the L_meet of P1 = the L_meet of P2
by A38, A40, BINOP_1:2;
hence
P1 = P2
by A38, A40, A43, BINOP_1:2; verum