let L be Lattice; :: thesis: for D1, D2 being non empty Subset of L holds D1 "/\" D2 = D2 "/\" D1
let D1, D2 be non empty Subset of L; :: thesis: D1 "/\" D2 = D2 "/\" D1

now :: thesis: for D1, D2 being non empty Subset of L holds D1 "/\" D2 c= D2 "/\" D1

let D1, D2 be non empty Subset of L; :: thesis: D1 "/\" D2 c= D2 "/\" D1
thus D1 "/\" D2 c= D2 "/\" D1 :: thesis: verum

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in D1 "/\" D2 or x in D2 "/\" D1 )
assume x in D1 "/\" D2 ; :: thesis: x in D2 "/\" D1
then ex p, q being Element of L st
( x = p "/\" q & p in D1 & q in D2 ) ;
hence x in D2 "/\" D1 ; :: thesis: verum

end;

end;

hence ( D1 "/\" D2 c= D2 "/\" D1 & D2 "/\" D1 c= D1 "/\" D2 ) ; :: according to XBOOLE_0:def 10 :: thesis: verum