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) "/\" Z) by A1, Def4
.= Z "/\" (Bottom L) by LATTICES:15
.= Bottom L by LATTICES:15 ;
hence Z "/\" X misses Z "/\" Y by Def4; :: thesis: verum