let L be 0_Lattice; :: thesis: for X, Y, Z being Element of L st X meets Y \ Z holds
X meets Y
let X, Y, Z be Element of L; :: thesis: ( X meets Y \ Z implies X meets Y )
assume X meets Y \ Z ; :: thesis: X meets Y
then X "/\" (Y \ Z) <> Bottom L by Def4;
then (X "/\" Y) "/\" (Z `) <> Bottom L by LATTICES:def 7;
then X "/\" Y <> Bottom L by LATTICES:15;
hence X meets Y by Def4; :: thesis: verum