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

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