let L be B_Lattice; :: thesis: for X, Y, Z being Element of L st X [= Y "\/" Z holds
X \ Y [= Z
let X, Y, Z be Element of L; :: thesis: ( X [= Y "\/" Z implies X \ Y [= Z )
assume X [= Y "\/" Z ; :: thesis: X \ Y [= Z
then X "/\" (Y ` ) [= (Y "\/" Z) "/\" (Y ` ) by LATTICES:27;
then X "/\" (Y ` ) [= (Y "/\" (Y ` )) "\/" (Z "/\" (Y ` )) by LATTICES:def 11;
then X \ Y [= (Bottom L) "\/" (Z "/\" (Y ` )) by LATTICES:47;
then A1: X \ Y [= Z "/\" (Y ` ) by LATTICES:39;
Z "/\" (Y ` ) [= Z by LATTICES:23;
hence X \ Y [= Z by A1, LATTICES:25; :: thesis: verum