let L be Lattice; :: thesis: for X, Y being Element of L st X meets Y holds
Y meets X
let X, Y be Element of L; :: thesis: ( X meets Y implies Y meets X )
assume X meets Y ; :: thesis: Y meets X
then X "/\" Y <> Bottom L by Def4;
hence Y meets X by Def4; :: thesis: verum