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:11;
then A1: (Y "\/" X) "/\" (Top L) [= Y "\/" Z by LATTICES:21;
X [= X "\/" Y by LATTICES:5;
hence X [= Y "\/" Z by A1, LATTICES:7; :: thesis: verum