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

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