let L be transitive antisymmetric with_infima RelStr ; :: thesis: for D1, D2, D3 being Subset of L holds (D1 "/\" D2) "/\" D3 = D1 "/\" (D2 "/\" D3)
let D1, D2, D3 be Subset of L; :: thesis: (D1 "/\" D2) "/\" D3 = D1 "/\" (D2 "/\" D3)
thus (D1 "/\" D2) "/\" D3 c= D1 "/\" (D2 "/\" D3) :: according to XBOOLE_0:def 10 :: thesis: D1 "/\" (D2 "/\" D3) c= (D1 "/\" D2) "/\" D3

proof

let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in (D1 "/\" D2) "/\" D3 or q in D1 "/\" (D2 "/\" D3) )
assume q in (D1 "/\" D2) "/\" D3 ; :: thesis: q in D1 "/\" (D2 "/\" D3)
then consider a1, b1 being Element of L such that
A1: q = a1 "/\" b1 and
A2: a1 in D1 "/\" D2 and
A3: b1 in D3 ;
consider a11, b11 being Element of L such that
A4: a1 = a11 "/\" b11 and
A5: a11 in D1 and
A6: b11 in D2 by A2;
( b11 "/\" b1 in D2 "/\" D3 & q = a11 "/\" (b11 "/\" b1) ) by A1, A3, A4, A6, LATTICE3:16;
hence q in D1 "/\" (D2 "/\" D3) by A5; :: thesis: verum

end;

let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in D1 "/\" (D2 "/\" D3) or q in (D1 "/\" D2) "/\" D3 )
assume q in D1 "/\" (D2 "/\" D3) ; :: thesis: q in (D1 "/\" D2) "/\" D3
then consider a1, b1 being Element of L such that
A7: ( q = a1 "/\" b1 & a1 in D1 ) and
A8: b1 in D2 "/\" D3 ;
consider a11, b11 being Element of L such that
A9: ( b1 = a11 "/\" b11 & a11 in D2 ) and
A10: b11 in D3 by A8;
( a1 "/\" a11 in D1 "/\" D2 & q = (a1 "/\" a11) "/\" b11 ) by A7, A9, LATTICE3:16;
hence q in (D1 "/\" D2) "/\" D3 by A10; :: thesis: verum