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 Y "\/" (X "/\" (Y ` )) [= Y "\/" Z by FILTER_0:1;
then (Y "\/" X) "/\" (Y "\/" (Y ` )) [= Y "\/" Z by LATTICES:31;
then (Y "\/" X) "/\" (Top L) [= Y "\/" Z by LATTICES:48;
then A1: X "\/" Y [= Y "\/" Z by LATTICES:43;
X [= X "\/" Y by LATTICES:22;
hence X [= Y "\/" Z by A1, LATTICES:25; :: thesis: verum