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 ;

( 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)

then A43:
the L_meet of P1 = the L_meet of P2
by A38, A40, BINOP_1:2;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;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

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

hence
P1 = P2
by A38, A40, A43, BINOP_1:2; :: thesis: verumlet 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;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