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 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:14;
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:14;
hence q in (D1 "\/" D2) "\/" D3 by A10; :: thesis: verum