let L be transitive antisymmetric with_suprema 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 set ; :: 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 & b1 in D3 ) ;
consider a11, b11 being Element of L such that
A3: a1 = a11 "\/" b11 and
A4: ( a11 in D1 & b11 in D2 ) by A2;
A5: b11 "\/" b1 in D2 "\/" D3 by A2, A4;
q = a11 "\/" (b11 "\/" b1) by A1, A3, LATTICE3:14;
hence q in D1 "\/" (D2 "\/" D3) by A4, A5; :: thesis: verum

end;

let q be set ; :: 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
A6: q = a1 "\/" b1 and
A7: ( a1 in D1 & b1 in D2 "\/" D3 ) ;
consider a11, b11 being Element of L such that
A8: b1 = a11 "\/" b11 and
A9: ( a11 in D2 & b11 in D3 ) by A7;
A10: a1 "\/" a11 in D1 "\/" D2 by A7, A9;
q = (a1 "\/" a11) "\/" b11 by A6, A8, LATTICE3:14;
hence q in (D1 "\/" D2) "\/" D3 by A9, A10; :: thesis: verum