let L be B_Lattice; :: thesis: for X, Y being Element of L holds (X "/\" Y) "\/" (X \ Y) = X
let X, Y be Element of L; :: thesis: (X "/\" Y) "\/" (X \ Y) = X
(X "/\" Y) "\/" (X \ Y) = ((X "/\" Y) "\/" X) "/\" ((X "/\" Y) "\/" (Y `)) by LATTICES:11
.= X "/\" ((X "/\" Y) "\/" (Y `)) by LATTICES:def 8
.= X "/\" ((X "\/" (Y `)) "/\" (Y "\/" (Y `))) by LATTICES:11
.= X "/\" ((X "\/" (Y `)) "/\" (Top L)) by LATTICES:21
.= X by LATTICES:def 9 ;
hence (X "/\" Y) "\/" (X \ Y) = X ; :: thesis: verum