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

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