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:31
.= X "/\" ((X "/\" Y) "\/" (Y ` )) by LATTICES:def 8
.= X "/\" ((X "\/" (Y ` )) "/\" (Y "\/" (Y ` ))) by LATTICES:31
.= X "/\" ((X "\/" (Y ` )) "/\" (Top L)) by LATTICES:48
.= X "/\" (X "\/" (Y ` )) by LATTICES:43
.= X by LATTICES:def 9 ;
hence (X "/\" Y) "\/" (X \ Y) = X ; :: thesis: verum