let L be Lattice; :: thesis: for X, Y being Element of st X meets Y holds
Y meets X
let X, Y be Element of ; :: 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