let L be 0_Lattice; :: thesis: for X, Y, Z being Element of L st X meets Y & Y [= Z holds
X meets Z
let X, Y, Z be Element of L; :: thesis: ( X meets Y & Y [= Z implies X meets Z )
assume that
A1: X meets Y and
A2: Y [= Z ; :: thesis: X meets Z
X "/\" Y <> Bottom L by A1, Def4;
then X "/\" Z <> Bottom L by A2, Th25, LATTICES:27;
hence X meets Z by Def4; :: thesis: verum