let L be Lattice; :: thesis: for X being Element of L holds
( X meets X iff X <> Bottom L )
let X be Element of L; :: thesis: ( X meets X iff X <> Bottom L )
A1: X "/\" X = X by LATTICES:18;

hereby :: thesis: ( X <> Bottom L implies X meets X )

assume X meets X ; :: thesis: X <> Bottom L
then X "/\" X <> Bottom L by Def4;
hence X <> Bottom L by LATTICES:18; :: thesis: verum

end;

assume X <> Bottom L ; :: thesis: X meets X
hence X meets X by A1, Def4; :: thesis: verum