let P1, P2 be strict Lattice; :: thesis: ( 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 ) ; :: thesis: P1 = P2
reconsider Z = the carrier of P1 as non empty set ;

now :: thesis: for x, y being Element of Z holds the L_meet of P1 . (x,y) = the L_meet of P2 . (x,y)

let x, y be Element of Z; :: thesis: the L_meet of P1 . (x,y) = the L_meet of P2 . (x,y)
y in Z ;
then A42: ex x3 being Relation of X,X st
( y = x3 & x3 is Equivalence_Relation of X ) by A38;
x in Z ;
then ex x2 being Relation of X,X st
( x = x2 & x2 is Equivalence_Relation of X ) by A38;
then reconsider x1 = x, y1 = y as Equivalence_Relation of X by A42;
thus the L_meet of P1 . (x,y) = x1 /\ y1 by A39
.= the L_meet of P2 . (x,y) by A41 ; :: thesis: verum

end;

then A43: the L_meet of P1 = the L_meet of P2 by A38, A40, BINOP_1:2;

now :: thesis: for x, y being Element of Z holds the L_join of P1 . (x,y) = the L_join of P2 . (x,y)

let x, y be Element of Z; :: thesis: the L_join of P1 . (x,y) = the L_join of P2 . (x,y)
y in Z ;
then A44: ex x3 being Relation of X,X st
( y = x3 & x3 is Equivalence_Relation of X ) by A38;
x in Z ;
then ex x2 being Relation of X,X st
( x = x2 & x2 is Equivalence_Relation of X ) by A38;
then reconsider x1 = x, y1 = y as Equivalence_Relation of X by A44;
thus the L_join of P1 . (x,y) = x1 "\/" y1 by A39
.= the L_join of P2 . (x,y) by A41 ; :: thesis: verum

end;

hence P1 = P2 by A38, A40, A43, BINOP_1:2; :: thesis: verum