let L be B_Lattice; :: thesis: for X, Y being Element of L holds (X "\/" Y) \ Y = X \ Y

let X, Y be Element of L; :: thesis: (X "\/" Y) \ Y = X \ Y

(X "\/" Y) \ Y = (X "/\" (Y `)) "\/" (Y "/\" (Y `)) by LATTICES:def 11

.= (X "/\" (Y `)) "\/" (Bottom L) by LATTICES:20

.= X "/\" (Y `) ;

hence (X "\/" Y) \ Y = X \ Y ; :: thesis: verum

let X, Y be Element of L; :: thesis: (X "\/" Y) \ Y = X \ Y

(X "\/" Y) \ Y = (X "/\" (Y `)) "\/" (Y "/\" (Y `)) by LATTICES:def 11

.= (X "/\" (Y `)) "\/" (Bottom L) by LATTICES:20

.= X "/\" (Y `) ;

hence (X "\/" Y) \ Y = X \ Y ; :: thesis: verum