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
A42: the carrier of P1 = { x where x is Relation of X,X : x is Equivalence_Relation of X } and
A43: 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
A44: the carrier of P2 = { x where x is Relation of X,X : x is Equivalence_Relation of X } and
A45: 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 ;

A46: now

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

end;

now

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

end;

then the L_meet of P1 = the L_meet of P2 by A42, A44, BINOP_1:2;
hence P1 = P2 by A42, A44, A46, BINOP_1:2; :: thesis: verum