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

let x, y be Element of Z; :: thesis:
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:

end;

let x, y be Element of Z; :: thesis:
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:

end;