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