let L be 0_Lattice; :: thesis: for X, Y, Z being Element of L st X misses Y holds
Z "/\" X misses Z "/\" Y
let X, Y, Z be Element of L; :: thesis: ( X misses Y implies Z "/\" X misses Z "/\" Y )
assume A1: X misses Y ; :: thesis: Z "/\" X misses Z "/\" Y
(Z "/\" X) "/\" (Z "/\" Y) = Z "/\" (X "/\" (Y "/\" Z)) by LATTICES:def 7
.= Z "/\" ((X "/\" Y) "/\" Z) by LATTICES:def 7
.= Z "/\" (Bottom L) by A1
.= Bottom L ;
hence Z "/\" X misses Z "/\" Y ; :: thesis: verum