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 ;
then (X "/\" Y) "/\" (Z `) <> Bottom L by LATTICES:def 7;
then X "/\" Y <> Bottom L ;
hence X meets Y ; :: thesis: verum