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

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