let L be B_Lattice; :: thesis: for X, Y, Z being Element of L st X [= Y holds
Z \ Y [= Z \ X
let X, Y, Z be Element of L; :: thesis: ( X [= Y implies Z \ Y [= Z \ X )
assume X [= Y ; :: thesis: Z \ Y [= Z \ X
then Y ` [= X ` by LATTICES:26;
hence Z \ Y [= Z \ X by LATTICES:9; :: thesis: verum