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:9;
then X "/\" (Y `) [= (Y "/\" (Y `)) "\/" (Z "/\" (Y `)) by LATTICES:def 11;
then A1: X \ Y [= (Bottom L) "\/" (Z "/\" (Y `)) by LATTICES:20;
Z "/\" (Y `) [= Z by LATTICES:6;
hence X \ Y [= Z by A1, LATTICES:7; :: thesis: verum